X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fdeclarative.ml;h=c669a4161defd736fde2cdd6d1774b3db095b911;hb=0978a9c19e672bb0b505f25737078409381700c7;hp=77276d92909866cfcba3c458c10f99eccc32f472;hpb=36014ac060f150e7d93f607c914a0b06239715c0;p=helm.git

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 77276d929..c669a4161 100644
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/components/tactics/declarative.ml
@@ -136,7 +136,7 @@ let andelim = existselim;;
 
 let rewritingstep ~dbd ~universe lhs rhs just last_step =
  let aux ((proof,goal) as status) =
-  let (curi,metasenv,proofbo,proofty) = proof in
+  let (curi,metasenv,proofbo,proofty, attrs) = proof in
   let _,context,gty = CicUtil.lookup_meta goal metasenv in
   let eq,trans =
    match LibraryObjects.eq_URI () with
@@ -196,7 +196,7 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step =
 	      FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context
                (Cic.Name name) ~typ
 	    in
-            let proof = curi,metasenv,proofbo,proofty in
+            let proof = curi,metasenv,proofbo,proofty, attrs in
             let proof,goals =
              ProofEngineTypes.apply_tactic
               (Tacticals.thens
@@ -225,6 +225,11 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step =
   ProofEngineTypes.mk_tactic aux
 ;;
 
+let we_proceed_by_cases_on t pat =
+ (*BUG here: pat unused *)
+ Tactics.cases_intros t
+;;
+
 let we_proceed_by_induction_on t pat =
  (*BUG here: pat unused *)
  Tactics.elim_intros ~depth:0 t