X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FeliminationTactics.ml;h=d05826ec0a514e962278afa6e69952bd8df919f7;hb=523a919017f8ec390d130c81de4897bd7c6d3a2c;hp=f1a9988eb96ea1adbdf447006f794039b10b2265;hpb=137a822662f81efbbeac7ddc833fc9ffe252a70e;p=helm.git

diff --git a/helm/software/components/tactics/eliminationTactics.ml b/helm/software/components/tactics/eliminationTactics.ml
index f1a9988eb..d05826ec0 100644
--- a/helm/software/components/tactics/eliminationTactics.ml
+++ b/helm/software/components/tactics/eliminationTactics.ml
@@ -58,7 +58,7 @@ let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None
 let rec scan_tac ~old_context_length ~index ~tactic =
    let scan_tac status =
       let (proof, goal) = status in
-      let _, metasenv, _, _ = proof in
+      let _, metasenv, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let context_length = List.length context in
       let rec aux index =
@@ -86,7 +86,7 @@ let rec check_types types = function
 let elim_clear_unfold_tac ~mk_fresh_name_callback ~types ~what =
    let elim_clear_unfold_tac status =
       let (proof, goal) = status in
-      let _, metasenv, _, _ = proof in
+      let _, metasenv, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let index, ty = H.lookup_type metasenv context what in
       match check_types types ty with 
@@ -136,7 +136,7 @@ let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[])
                   ?(user_types=[]) ?what ~dbd =
    let decompose_tac status =
       let (proof, goal) = status in
-      let _, metasenv,_,_ = proof in
+      let _, metasenv,_,_, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let types = List.rev_append user_types (FwdQueries.decomposables dbd) in
       let tactic = elim_clear_unfold_tac ~mk_fresh_name_callback ~types in