X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Ftacticals.ml;h=c6fbc36a40594cf0b3aa0f23fede5cf72f48ae1b;hb=0978a9c19e672bb0b505f25737078409381700c7;hp=28bd71b2da5901c199114dde8ce8bacf79aaa17f;hpb=4885f49660dc31fc6ecbed36c383b111381a8684;p=helm.git

diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml
index 28bd71b2d..c6fbc36a4 100644
--- a/helm/software/components/tactics/tacticals.ml
+++ b/helm/software/components/tactics/tacticals.ml
@@ -42,7 +42,7 @@ module PET = ProofEngineTypes
 
 let id_tac = 
  let id_tac (proof,goal) = 
-  let _, metasenv, _, _ = proof in
+  let _, metasenv, _, _, _ = proof in
   let _, _, _ = CicUtil.lookup_meta goal metasenv in
   (proof,[goal])
  in 
@@ -50,7 +50,7 @@ let id_tac =
 
 let fail_tac =
  let fail_tac (proof,goal) =
-  let _, metasenv, _, _ = proof in
+  let _, metasenv, _, _, _ = proof in
   let _, _, _ = CicUtil.lookup_meta goal metasenv in
    raise (PET.Fail (lazy "fail tactical"))
  in
@@ -293,7 +293,7 @@ struct
   let progress_tactic ~tactic =
     let msg = lazy "Failed to progress" in
     let get_sequent (proof, goal) =
-      let (_, metasenv, _, _) = proof in
+      let (_, metasenv, _, _, _) = proof in
       let _, context, ty = CicUtil.lookup_meta goal metasenv in
       context, ty
     in