on différencie exact pour les preuves et pour les termes

proof.ml

@@ -16,7 +16,8 @@ type goal = hlam * Types.ty * context
 type proof = goal option * goal list
 
 type tactic =
-  Exact of lam
+  Exact_term of lam
+  | Exact_proof of id
   | Assumption
   | Intro
   | Cut of ty
@@ -68,6 +69,13 @@ let rec lam_of_hlam : hlam -> lam = function
   | Ref e_ref -> lam_of_hlam !e_ref
   | Hole -> failwith "can not translate unclosed terms"
 
+
+let rec get_term_by_id (hyp : id) : context -> hlam option =
+  function
+  [] -> None
+  | (hyp', h, _) :: _ when hyp' = hyp -> Some h
+  | _ :: cs -> get_term_by_id hyp cs
+
 let rec get_term_by_type (ty : Types.ty) : context -> hlam option =
   function
   [] -> None
@@ -86,7 +94,15 @@ let tact_exact_term ((g, gs) : proof) (e : lam) : proof =
     fill h (hlam_of_lam e);
     next_goal gs
 
-let tact_exact_proof ((g, gs) : proof) (h : id) : proof =
+let tact_exact_proof ((g, gs) : proof) (hyp : id) : proof =
+  match g with
+  None -> failwith "no current goal"
+  | Some (h, _, cs) ->
+    match get_term_by_id hyp cs with
+    Some h' ->
+      fill h h';
+      next_goal gs
+    | None -> raise TacticFailed
 
 let tact_assumption ((g, gs) : proof) : proof =
   match g with
@@ -154,9 +170,10 @@ let tact_intros : proof -> proof =
 let tact_try (p : proof) (t : tactic) : proof =
   try
   match t with
-  Exact e -> tact_exact p e
+  Exact_term e -> tact_exact_term p e
+  | Exact_proof hyp -> tact_exact_proof p hyp
   | Intro -> tact_intro p
   | Assumption -> tact_assumption p
   | Cut t -> tact_cut p t
-  | Apply h -> tact_apply p e
+  | Apply h -> tact_apply p h
   with TacticFailed -> p