added a (for the moment) dummy field _subst to ProofengineTypes.proof.

[helm.git] / components / tactics / declarative.ml

diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index e36c860374cc8e109ec4d35068b1d87f3ea8ce5f..2f012ed40d9eded87bf8fcf62c6c0dd929aafac6 100644 (file)
--- a/components/tactics/declarative.ml
+++ b/components/tactics/declarative.ml
@@ -123,10 +123,10 @@ let we_need_to_prove t id ty =
 
 let existselim ~dbd ~universe t id1 t1 id2 t2 =
  let aux (proof, goal) = 
-  let (n,metasenv,bo,ty,attrs) = proof in
+  let (n,metasenv,_subst,bo,ty,attrs) = proof in
   let metano,context,_ = CicUtil.lookup_meta goal metasenv in
   let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in
-  let proof' = (n,metasenv,bo,ty,attrs) in
+  let proof' = (n,metasenv,_subst,bo,ty,attrs) in
    ProofEngineTypes.apply_tactic (
    Tacticals.thens
     ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/ex.ind", 0, []); t1 ; Cic.Lambda (Cic.Name id1, t1, t2)]))
@@ -155,7 +155,7 @@ let andelim t id1 t1 id2 t2 =
 
 let rewritingstep ~dbd ~universe lhs rhs just last_step =
  let aux ((proof,goal) as status) =
-  let (curi,metasenv,proofbo,proofty, attrs) = proof in
+  let (curi,metasenv,_subst,proofbo,proofty, attrs) = proof in
   let _,context,gty = CicUtil.lookup_meta goal metasenv in
   let eq,trans =
    match LibraryObjects.eq_URI () with
@@ -221,7 +221,7 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step =
              FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context
                (Cic.Name name) ~typ
            in
-            let proof = curi,metasenv,proofbo,proofty, attrs in
+            let proof = curi,metasenv,_subst,proofbo,proofty, attrs in
             let proof,goals =
              ProofEngineTypes.apply_tactic
               (Tacticals.thens