diff --git a/hlam.ml b/hlam.ml
index e04f803..aa81c62 100644
--- a/hlam.ml
+++ b/hlam.ml
@@ -14,6 +14,7 @@ type hlam = (* hollow lam *)
   | Hole
 
 
+(* avec assoc la liste d'associations anciennes ref -> nouvelles ref, remplacer toutes les ref *)
 let clean_hlam assoc (h : hlam) : hlam =
   let rec clean (h : hlam) : hlam= match h with
     HFun ((s, t), h) -> HFun ((s, t), clean h)
diff --git a/main.ml b/main.ml
index cb5b6a0..26c4894 100644
--- a/main.ml
+++ b/main.ml
@@ -44,7 +44,9 @@ let rec beta_reduce (l : Lam.lam) =
   | None -> l
   | Some l' -> beta_reduce l'
 
+(* copier l'entièreté de l'état d'une preuve avec de nouvelles références pour le Undo *)
 let clean_state ((s, p) : interactive_state) =
+  (* assoc fait le lien entre les anciennes et nouvelles ref, doit être commun au terme et aux différents composants de la preuve *)
   let assoc, new_p = clean_proof p in
   match s with
   | None -> None, new_p
@@ -114,19 +116,19 @@ let rec interactive (get_instr : unit -> instr) (sl : (interactive_state) list)
     | s::sq -> s, sq
   in
   begin
-    let _ = match g with
+    let _ = match g with (* affichage de l'état de la preuve *)
     None -> print_string "\n\027[1mNo more goals.\027[0m\n"
     | Some g' -> print_newline (); print_goal g'
     in
 
     try
-      match get_instr () with
+      match get_instr () with (* get_instr récupère l'instruction suivante depuis un fichier ou stdin (garde en buffer les lignes doubles notamment) *)
       Cmd c ->
         begin match c with
         Goal ty ->
           let rh = Ref (ref Hole) in
           [Some (rh, ty), (Some (rh, ty, []), [])] |> interactive get_instr
-        | Undo -> interactive get_instr sq
+        | Undo -> interactive get_instr sq (* pour Undo, on appelle juste interactive en supprimant le dernier état *)
         | Qed -> begin match cg with
           None ->
             print_error "No current goal" "";
@@ -163,6 +165,8 @@ let rec interactive (get_instr : unit -> instr) (sl : (interactive_state) list)
           end
         end
       | Tact t ->
+        (* on applique la tactique et on copie l'état actuel de la preuve pour un futur Undo
+           Comme OCaml évalue de la droite vers la gauche, on fait bien la copie avant de modifier les références dans la preuve *)
         (cg, (apply_tactic (g, gs) t))::(clean_state (cg, (g, gs)))::sq |> interactive get_instr
     with
       Parser.Error ->
@@ -214,7 +218,7 @@ let recupere_entree () =
     else Simple begin
     let cmd_buff = ref [] in
       if !nom_fichier = "" then
-        (
+        ((* récupérer les commandes depuis stdin, les lignes vides sont considérées comme des erreurs *)
           fun () ->
           match !cmd_buff with
           | [] ->
@@ -227,7 +231,7 @@ let recupere_entree () =
           | e::q -> cmd_buff := q; e
         )
       else
-        (
+        ((* récupérer les commandes depuis un fichier *)
           fun () ->
           match !cmd_buff with
           | [] ->