X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FdiscriminationTactics.ml;h=9d83ad595e8af2dfa6712afcfb04b0415f6fb7ae;hb=e1f0bb910f75b8b21f2c5e394ebb4c5a63ef4945;hp=ccbf17ae643df6a099d7e99309da3c5356bd010e;hpb=12fe61bed1275c4c596501fb951a9197f50c93e8;p=helm.git

diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml
index ccbf17ae6..9d83ad595 100644
--- a/helm/software/components/tactics/discriminationTactics.ml
+++ b/helm/software/components/tactics/discriminationTactics.ml
@@ -145,7 +145,7 @@ let discriminate_tac ~term =
  in
  let discriminate'_tac ~term status = 
   let (proof, goal) = status in
-  let _,metasenv,_,_, _ = proof in
+  let _,metasenv,_subst,_,_, _ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
   let termty,_ = 
     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
@@ -228,7 +228,7 @@ let rec injection_tac ~first_time ~term ~liftno ~continuation =
  in
  let injection_tac ~term status = 
   let (proof, goal) = status in
-  let _,metasenv,_,_, _ = proof in
+  let _,metasenv,_subst, _,_, _ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
   let term = CicSubstitution.lift liftno term in
   let termty,_ = 
@@ -335,7 +335,7 @@ and injection1_tac ~term ~i ~liftno ~continuation =
    * differiscono (o potrebbero differire?) nell'i-esimo parametro 
    * del costruttore *)
   let term = CicSubstitution.lift liftno term in
-  let _,metasenv,_,_, _ = proof in
+  let _,metasenv,_subst,_,_, _ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
   let termty,_ = 
     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
@@ -467,7 +467,7 @@ and injection1_tac ~term ~i ~liftno ~continuation =
                     (fun status ->    
                       debug_print (lazy "riempo il cut"); 
                       let (proof, goal) = status in
-                      let _,metasenv,_,_, _ = proof in
+                      let _,metasenv,_subst,_,_, _ = proof in
                       let _,context,gty =CicUtil.lookup_meta goal metasenv in
                       let gty = Unshare.unshare gty in
                       let new_t1' =