X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=3b958c2c24ff1756e9ab3296380dc7d78f070b97;hb=8aaf525856e25bcd8f355e505fd00f45c62bc18f;hp=feb161d7fe84aaa022271e5d7338b839a0f9e17b;hpb=358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index feb161d7f..3b958c2c2 100644
--- 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: