beginning of the tactics lapply and fwd

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index feb161d7fe84aaa022271e5d7338b839a0f9e17b..3b958c2c24ff1756e9ab3296380dc7d78f070b97 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -413,6 +413,10 @@ EXTEND
     | [ IDENT "transitivity" ];
       t = tactic_term ->
         TacticAst.Transitivity (loc, t)
+    | [ IDENT "fwd" ]; name = IDENT ->
+        TacticAst.FwdSimpl (loc, name)
+    | [ IDENT "lapply" ]; t = term ->
+        TacticAst.LApply (loc, t, [])
     ]
   ];
   tactical: