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

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

diff --git a/helm/software/components/tactics/tactics.ml b/helm/software/components/tactics/tactics.ml
index c34355b8ea21fd382dcfa08c9d0e9cc728056ab7..82c343085a0c0b4ec38e35693db54acfebd4a8b5 100644 (file)
--- a/helm/software/components/tactics/tactics.ml
+++ b/helm/software/components/tactics/tactics.ml
@@ -30,6 +30,7 @@ let apply = PrimitiveTactics.apply_tac
 let applyS = Auto.applyS_tac
 let assumption = VariousTactics.assumption_tac
 let auto = AutoTactic.auto_tac
+let cases_intros = PrimitiveTactics.cases_intros_tac
 let change = ReductionTactics.change_tac
 let clear = ProofEngineStructuralRules.clear
 let clearbody = ProofEngineStructuralRules.clearbody