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

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

diff --git a/components/tactics/eliminationTactics.ml b/components/tactics/eliminationTactics.ml
index f18d2b333b68b322523b656db7db9527816c7324..29961db389d1c3a039b23286b4eb643f075a0146 100644 (file)
--- a/components/tactics/eliminationTactics.ml
+++ b/components/tactics/eliminationTactics.ml
@@ -91,7 +91,7 @@ let rec check_type sorts metasenv context t =
 let rec scan_tac ~old_context_length ~index ~tactic =
    let scan_tac status =
       let (proof, goal) = status in
-      let _, metasenv, _, _, _ = proof in
+      let _, metasenv, _subst, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let context_length = List.length context in
       let rec aux index =
@@ -111,7 +111,7 @@ let rec scan_tac ~old_context_length ~index ~tactic =
 let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what =
    let elim_clear_unfold_tac status =
       let (proof, goal) = status in
-      let _, metasenv, _, _, _ = proof in
+      let _, metasenv, _subst, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let index, ty = PEH.lookup_type metasenv context what in
       let tac = 
@@ -159,7 +159,7 @@ let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort C.CProp])
                   ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () =
    let decompose_tac status =
       let (proof, goal) = status in
-      let _, metasenv,_,_, _ = proof in
+      let _, metasenv, _subst, _,_, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let tactic = elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback in
       let old_context_length = List.length context in