From 00c1a116d166754f0f954559f9481e8f4dae58b3 Mon Sep 17 00:00:00 2001
From: Marwan <marwan.azizi@ens-lyon.fr>
Date: Tue, 14 May 2024 15:55:19 +0200
Subject: [PATCH] =?UTF-8?q?tactique=20apply=20g=C3=A9n=C3=A9ralis=C3=A9e,?=
 =?UTF-8?q?=20=C3=A0=20commenter?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 proof.ml | 26 ++++++++++++++------------
 1 file changed, 14 insertions(+), 12 deletions(-)

diff --git a/proof.ml b/proof.ml
index b96f91a..133deaf 100644
--- a/proof.ml
+++ b/proof.ml
@@ -217,21 +217,21 @@ let tact_apply ((g, gs) : proof) (hyp_id : id) : proof =
     | _ -> false
   in
   let rec generate_goals (goal_ty : ty) (impl_ty : ty) (impl_h : hlam)
-  (goal_h : hlam) (cs : context) (gs : goal list) : proof =
+  (goal_h : hlam) (h : hlam) (cs : context) (gs : goal list) : proof =
     match impl_ty with
     Arr (t1, t2) when t2 = goal_ty ->
       let sub_h = Ref (ref Hole) in
-      let _ = fill goal_h (HApp (impl_h, sub_h)) in
+      let _ = fill h sub_h in
+      let _ = fill goal_h impl_h in
       Some (sub_h, t1, cs), gs
     | Arr (t1, t2) ->
-      (* nouveau sous but *)
-      let sub_h = Ref (ref Hole) in (* preuve de t1 *)
-      let new_h = Ref (ref Hole) in (* suite de l'implication *)
-      let _ = fill impl_h (HApp (HApp (impl_h, sub_h), new_h)) in
+      let sub_h = Ref (ref Hole) in
+      let new_h = Ref (ref Hole) in
+      let _ = fill h sub_h in
+      let impl_h = HApp (impl_h, new_h) in
       let gs = (sub_h, t1, cs) :: gs in
-      generate_goals goal_ty t2 new_h goal_h cs gs
+      generate_goals goal_ty t2 impl_h goal_h new_h cs gs
     | _ -> failwith "impossible"
-      
   in
   let rec get_hyp : context -> (hlam * ty) = function
     [] -> raise (TacticFailed "no such hypothesis in context")
@@ -240,10 +240,12 @@ let tact_apply ((g, gs) : proof) (hyp_id : id) : proof =
   in
   match g with
   None -> raise (TacticFailed "no current goal")
-  | Some (h, goal_ty, cs) ->
-    let h', t' = get_hyp cs in
-    if is_implied goal_ty t'
-    then generate_goals goal_ty t' h' h cs gs
+  | Some (goal_h, goal_ty, cs) ->
+    let impl_h, impl_ty = get_hyp cs in
+    let new_h = Ref (ref Hole) in
+    let impl_h_2 = HApp (impl_h, new_h) in
+    if is_implied goal_ty impl_ty
+    then generate_goals goal_ty impl_ty impl_h_2 goal_h new_h cs gs
     else raise (TacticFailed "not an implication")
 
 let tact_intros : proof -> proof =