Unified refactored

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

diff --git a/components/tactics/eliminationTactics.ml b/components/tactics/eliminationTactics.ml
index f1a9988eb96ea1adbdf447006f794039b10b2265..d05826ec0a514e962278afa6e69952bd8df919f7 100644 (file)
--- a/components/tactics/eliminationTactics.ml
+++ b/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