LexiconAstPp: fixed syntax for include

[helm.git] / components / tactics / declarative.ml

diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index 77276d92909866cfcba3c458c10f99eccc32f472..c669a4161defd736fde2cdd6d1774b3db095b911 100644 (file)
--- a/components/tactics/declarative.ml
+++ b/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