New declarative tactic "we proceed by cases on t to prove t'".

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

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