X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FprimitiveTactics.ml;h=aeb0c0751286285b637a1cff94aae6854ee3cae4;hb=c6cc2a7227d6750076f591a62d7b1896ebf1ebfa;hp=c5aab0f5ff45eeebb63f608195552302d799df26;hpb=1acfe506c30e7fcc9d6e427d2523130c371a1159;p=helm.git

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index c5aab0f5f..aeb0c0751 100644
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -261,7 +261,7 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
  let module T = CicTypeChecker in
  let module R = CicReduction in
  let module C = Cic in
-  let (_,metasenv,_,_, _) = proof in
+  let (_,metasenv,_subst,_,_, _) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in
    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
@@ -325,7 +325,7 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
    let subst_in =
      (* if we just apply the subtitution, the type is irrelevant:
               we may use Implicit, since it will be dropped *)
-     CicMetaSubst.apply_subst ((metano,(context,bo',Cic.Implicit None))::subst)
+      ((metano,(context,bo',Cic.Implicit None))::subst)
    in
    let (newproof, newmetasenv''') = 
     ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in
@@ -373,7 +373,7 @@ let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_
  =
   let module C = Cic in
   let module R = CicReduction in
-   let (_,metasenv,_,_, _) = proof in
+   let (_,metasenv,_subst,_,_, _) = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
     let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
      let (context',ty',bo') =
@@ -393,7 +393,7 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:
   term (proof, goal)
  =
   let module C = Cic in
-   let curi,metasenv,pbo,pty, attrs = proof in
+   let curi,metasenv,_subst,pbo,pty, attrs = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
     let newmeta1 = ProofEngineHelpers.new_meta_of_proof ~proof in
     let newmeta2 = newmeta1 + 1 in
@@ -428,7 +428,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
   term (proof, goal)
  =
   let module C = Cic in
-   let curi,metasenv,pbo,pty, attrs = proof in
+   let curi,metasenv,_subst,pbo,pty, attrs = proof in
    (* occur check *)
    let occur i t =
      let m = CicUtil.metas_of_term t in 
@@ -464,7 +464,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
 let exact_tac ~term =
  let exact_tac ~term (proof, goal) =
   (* Assumption: the term bo must be closed in the current context *)
-  let (_,metasenv,_,_, _) = proof in
+  let (_,metasenv,_subst,_,_, _) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let module T = CicTypeChecker in
   let module R = CicReduction in
@@ -497,7 +497,7 @@ module RT  = ReductionTactics
 let beta_after_elim_tac upto predicate =
    let beta_after_elim_tac status =
       let proof, goal = status in
-      let _, metasenv, _, _, _ = proof in
+      let _, metasenv, _subst, _, _, _ = proof in
       let _, _, ty = CicUtil.lookup_meta goal metasenv in
       let mk_pattern ~equality ~upto ~predicate ty =
          (* code adapted from ProceduralConversion.generalize *)
@@ -564,7 +564,7 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
       | _                    -> raise (PET.Fail (lazy "not implemented"))
    in    
    let ugraph = CicUniv.empty_ugraph in
-   let curi, metasenv, proofbo, proofty, attrs = proof in
+   let curi, metasenv, _subst, proofbo, proofty, attrs = proof in
    let conjecture = CicUtil.lookup_meta goal metasenv in
    let metano, context, ty = conjecture in 
     let termty,_ugraph = TC.type_of_aux' metasenv context term ugraph in
@@ -686,13 +686,13 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
          ProofEngineHelpers.compare_metasenvs
             ~oldmetasenv:metasenv ~newmetasenv:metasenv''
       in
-      let proof' = curi,metasenv'',proofbo,proofty, attrs in
+      let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in
       let proof'', new_goals' =
          PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal)
       in
       (* The apply_tactic can have closed some of the new_goals *)
       let patched_new_goals =
-         let (_,metasenv''',_,_, _) = proof'' in
+         let (_,metasenv''',_subst,_,_, _) = proof'' in
          List.filter
             (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
 	    new_goals @ new_goals'
@@ -714,7 +714,7 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera
   let module U = UriManager in
   let module R = CicReduction in
   let module C = Cic in
-  let (curi,metasenv,proofbo,proofty, attrs) = proof in
+  let (curi,metasenv,_subst, proofbo,proofty, attrs) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
   let termty = CicReduction.whd context termty in
@@ -825,13 +825,13 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera
     ProofEngineHelpers.compare_metasenvs
       ~oldmetasenv:metasenv ~newmetasenv:metasenv''
   in
-  let proof' = curi,metasenv'',proofbo,proofty, attrs in
+  let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in
   let proof'', new_goals' =
     PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal)
   in
   (* The apply_tactic can have closed some of the new_goals *)
   let patched_new_goals =
-    let (_,metasenv''',_,_,_) = proof'' in
+    let (_,metasenv''',_subst,_,_,_) = proof'' in
       List.filter
         (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
         new_goals @ new_goals'
@@ -866,7 +866,7 @@ let letout_tac =
    let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
    let term = C.Sort C.Set in
    let letout_tac (proof, goal) =
-      let curi, metasenv, pbo, pty, attrs = proof in
+      let curi, metasenv, _subst, pbo, pty, attrs = proof in
       let metano, context, ty = CicUtil.lookup_meta goal metasenv in
       let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
       let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in