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

[helm.git] / components / grafite_engine / grafiteEngine.ml

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index 082eee5f95279cbb5265197849220bd3082e3311..a125d23be41c79f212c8e5b0999753ec6d101888 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -172,6 +172,8 @@ let tactic_of_ast status ast =
   | GrafiteAst.Bydone (_, t) ->
      Declarative.bydone ~dbd:(LibraryDb.instance())
       ~universe:status.GrafiteTypes.universe t
+  | GrafiteAst.We_proceed_by_cases_on (_, t, t1) ->
+     Declarative.we_proceed_by_cases_on t t1
   | GrafiteAst.We_proceed_by_induction_on (_, t, t1) ->
      Declarative.we_proceed_by_induction_on t t1
   | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction t id