From 359d7333f50c90d91216392a9370acd41c19f1e5 Mon Sep 17 00:00:00 2001
From: Adrien Vannson <adrien.vannson@protonmail.com>
Date: Tue, 10 May 2022 15:20:50 +0200
Subject: [PATCH] Commentaire

---
 main.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/main.ml b/main.ml
index 31bc94e..94ea82f 100644
--- a/main.ml
+++ b/main.ml
@@ -148,11 +148,12 @@ while !subgoals <> [] do
               | None -> failwith ("Hypothesis " ^ var ^ " not found")
               | _ -> failwith ("Hypothesis " ^ var ^ " unusable")
         )
+      (* Pour montrer A, on montre B -> A et B *)
       | Cut tint -> (
-            subgoals := (TImpl(tint, ty), hyps)::(tint, hyps)::!subgoals;
-            fill_holes := function 
-                | (pf::px::s) -> f ((LApp(pf, px))::s)
-                | _ -> fail ()
+            subgoals := (TImpl (tint, ty), hyps) :: (tint, hyps) :: !subgoals;
+            fill_holes := function
+              | pf :: px :: s -> f ((LApp (pf, px)) :: s)
+              | _ -> fail ()
         )
 done;