Corrected a bug with holes in proofs

4 files changed, 17 insertions, 15 deletions

diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 87b5cb7..d8ec105 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -369,9 +369,7 @@ let make_proof call_solver rt ro rf l =
   call_solver rt ro fl (root,l)
 
 
-let tactic call_solver rt ro ra rf env sigma t =
-  let (forall_let, concl) = Term.decompose_prod_assum t in
-  let env = Environ.push_rel_context forall_let env in
+let core_tactic call_solver rt ro ra rf env sigma concl =
   let a, b = get_arguments concl in
   let (body_cast, body_nocast, cuts) =
     if ((Term.eq_constr b (Lazy.force ctrue)) || (Term.eq_constr b (Lazy.force cfalse))) then
@@ -386,16 +384,17 @@ let tactic call_solver rt ro ra rf env sigma t =
       let max_id_confl = make_proof call_solver rt ro rf l in
       build_body_eq rt ro ra rf (Form.to_coq l1) (Form.to_coq l2) (Form.to_coq l) max_id_confl in
 
-  let compose_lam_assum forall_let body =
-    List.fold_left (fun t rd -> Term.mkLambda_or_LetIn rd t) body forall_let in
-  let res_cast = compose_lam_assum forall_let body_cast in
-  let res_nocast = compose_lam_assum forall_let body_nocast in
-
   let cuts = (Btype.get_cuts rt)@cuts in
 
   List.fold_right (fun (eqn, eqt) tac ->
       Structures.tclTHENLAST (Structures.assert_before (Names.Name eqn) eqt) tac
     ) cuts
       (Structures.tclTHEN
-         (Structures.set_evars_tac res_nocast)
-         (Structures.vm_cast_no_check res_cast))
+         (Structures.set_evars_tac body_nocast)
+         (Structures.vm_cast_no_check body_cast))
+
+
+let tactic call_solver rt ro ra rf =
+  Structures.tclTHEN
+    Tactics.intros
+    (Structures.mk_tactic (core_tactic call_solver rt ro ra rf))
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 48ae312..e7ad9b1 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -149,10 +149,10 @@ let call_verit rt ro fl root =
     | VeritSyntax.Sat -> Structures.error "veriT can't prove this"
 
 
-let tactic env sigma t =
+let tactic () =
   clear_all ();
   let rt = Btype.create () in
   let ro = Op.create () in
   let ra = VeritSyntax.ra in
   let rf = VeritSyntax.rf in
-  SmtCommands.tactic call_verit rt ro ra rf env sigma t
+  SmtCommands.tactic call_verit rt ro ra rf
diff --git a/src/versions/standard/smtcoq_plugin_standard.ml4 b/src/versions/standard/smtcoq_plugin_standard.ml4
index b714029..6ae3545 100644
--- a/src/versions/standard/smtcoq_plugin_standard.ml4
+++ b/src/versions/standard/smtcoq_plugin_standard.ml4
@@ -50,9 +50,9 @@ END
 
 
 TACTIC EXTEND Tactic_zchaff
-| [ "zchaff" ] -> [ Structures.mk_tactic Zchaff.tactic ]
+| [ "zchaff" ] -> [ Zchaff.tactic () ]
 END
 
 TACTIC EXTEND Tactic_verit
-| [ "verit" ] -> [ Structures.mk_tactic Verit.tactic ]
+| [ "verit" ] -> [ Verit.tactic () ]
 END
diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml
index bd656aa..106c0b5 100644
--- a/src/zchaff/zchaff.ml
+++ b/src/zchaff/zchaff.ml
@@ -514,7 +514,7 @@ let make_proof pform_tbl atom_tbl env reify_form l =
 
 (* The whole tactic *)
 
-let tactic env sigma t =
+let core_tactic env sigma t =
   SmtTrace.clear ();
 
   let (forall_let, concl) = Term.decompose_prod_assum t in
@@ -548,3 +548,6 @@ let tactic env sigma t =
   (Structures.tclTHEN
      (Structures.set_evars_tac res_nocast)
      (Structures.vm_cast_no_check res_cast))
+
+
+let tactic () = Structures.tclTHEN Tactics.intros (Structures.mk_tactic core_tactic)