X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FdiscriminationTactics.ml;h=5f3e16d370f18c771c35878d544f33784589a4dc;hb=54d09097e4ddbf7383d47ff0df4f1d9e14ea50fc;hp=ebf7728449dad2d03de6b08744529171c667ae34;hpb=5f00ef380aafdaae93a40a3a47491d43ec9c3a62;p=helm.git

diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml
index ebf772844..5f3e16d37 100644
--- a/helm/software/components/tactics/discriminationTactics.ml
+++ b/helm/software/components/tactics/discriminationTactics.ml
@@ -142,7 +142,7 @@ let discriminate_tac ~term =
  in
  let discriminate'_tac ~term status = 
   let (proof, goal) = status in
-  let _,metasenv,_,_ = proof in
+  let _,metasenv,_,_, _ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
   let termty,_ = 
     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
@@ -201,7 +201,7 @@ let rec injection_tac ~first_time ~term ~liftno ~continuation =
   let module U = UriManager in
   let module P = PrimitiveTactics in
   let module T = Tacticals in
-  let _,metasenv,_,_ = proof in
+  let _,metasenv,_,_, _ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
   let term = CicSubstitution.lift liftno term in
   let termty,_ = (* TASSI: FIXME *)
@@ -307,7 +307,7 @@ and injection1_tac ~term ~i ~liftno ~continuation =
    let module P = PrimitiveTactics in
    let module T = Tacticals in
    let term = CicSubstitution.lift liftno term in
-   let _,metasenv,_,_ = proof in
+   let _,metasenv,_,_, _ = proof in
    let _,context,_ = CicUtil.lookup_meta goal metasenv in
    let termty,_ = (* TASSI: FIXME *)
      CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
@@ -424,7 +424,7 @@ and injection1_tac ~term ~i ~liftno ~continuation =
                        ~start:(ProofEngineTypes.mk_tactic 
                          (fun status ->    
                            let (proof, goal) = status in
-                           let _,metasenv,_,_ = proof in
+                           let _,metasenv,_,_, _ = proof in
                             let _,context,gty =
                              CicUtil.lookup_meta goal metasenv
                             in