X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FeliminationTactics.ml;h=29961db389d1c3a039b23286b4eb643f075a0146;hb=fbdd1cc46819d19ed135391a4a954c19d1b92c0c;hp=f18d2b333b68b322523b656db7db9527816c7324;hpb=a1c4c601850c71e094a4703af00f02ca2026d8ed;p=helm.git

diff --git a/components/tactics/eliminationTactics.ml b/components/tactics/eliminationTactics.ml
index f18d2b333..29961db38 100644
--- 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