X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FprimitiveTactics.ml;h=3ef39d0c512dbb52c6b35398b78d1199ca02dc83;hb=8465f33f9ad62040f41a2a2604745cda11725d98;hp=2e9a3db33f9204afa1ab3ccccb19a96f43f06af0;hpb=87958f30640584c3c9de3adc49b08ab7675332ad;p=helm.git

diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml
index 2e9a3db33..3ef39d0c5 100644
--- a/components/tactics/primitiveTactics.ml
+++ b/components/tactics/primitiveTactics.ml
@@ -251,7 +251,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,_,_, _) = 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' =
@@ -365,7 +365,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,_,_, _) = 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') =
@@ -385,7 +385,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 = proof in
+   let curi,metasenv,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
@@ -420,7 +420,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 = proof in
+   let curi,metasenv,pbo,pty, attrs = proof in
    (* occur check *)
    let occur i t =
      let m = CicUtil.metas_of_term t in 
@@ -456,7 +456,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,_,_, _) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let module T = CicTypeChecker in
   let module R = CicReduction in
@@ -480,7 +480,7 @@ let elim_tac ~term =
   let module U = UriManager in
   let module R = CicReduction in
   let module C = Cic in
-   let (curi,metasenv,proofbo,proofty) = proof in
+   let (curi,metasenv,proofbo,proofty, attrs) = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
     let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
     let termty = CicReduction.whd context termty in
@@ -544,13 +544,13 @@ let elim_tac ~term =
             ProofEngineHelpers.compare_metasenvs
              ~oldmetasenv:metasenv ~newmetasenv:metasenv''
            in
-           let proof' = curi,metasenv'',proofbo,proofty in
+           let proof' = curi,metasenv'',proofbo,proofty, attrs in
             let proof'', new_goals' =
              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''',_,_, _) = proof'' in
                List.filter
                 (function i -> List.exists (function (j,_,_) -> j=i) metasenv'''
                 ) new_goals @ new_goals'
@@ -566,7 +566,7 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam
   let module U = UriManager in
   let module R = CicReduction in
   let module C = Cic in
-   let (curi,metasenv,proofbo,proofty) = proof in
+   let (curi,metasenv,proofbo,proofty, attrs) = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
     let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
     let termty = CicReduction.whd context termty in
@@ -628,7 +628,6 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam
        let term_to_refine =
         C.MutCase (uri,typeno,outtype,term,patterns)
        in
-prerr_endline (CicMetaSubst.ppterm_in_context ~metasenv:metasenv' [] term_to_refine context);
         let refined_term,_,metasenv'',_ = 
          CicRefine.type_of_aux' metasenv' context term_to_refine
            CicUniv.empty_ugraph
@@ -637,13 +636,13 @@ prerr_endline (CicMetaSubst.ppterm_in_context ~metasenv:metasenv' [] term_to_ref
           ProofEngineHelpers.compare_metasenvs
            ~oldmetasenv:metasenv ~newmetasenv:metasenv''
          in
-         let proof' = curi,metasenv'',proofbo,proofty in
+         let proof' = curi,metasenv'',proofbo,proofty, attrs in
           let proof'', new_goals' =
            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''',_,_,_) = proof'' in
              List.filter
               (function i -> List.exists (function (j,_,_) -> j=i) metasenv'''
               ) new_goals @ new_goals'
@@ -680,7 +679,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 = proof in
+      let curi, metasenv, 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