]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/cicTextualParser2.ml
fixed LApply pretty printing
[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml
index e54185a1b2fd9e368673caa9f923c30c12bbfe4a..d3d6e28aebcbb4377d9ad343774b89b16b4ba601 100644 (file)
@@ -417,8 +417,9 @@ EXTEND
         TacticAst.Transitivity (loc, t)
     | [ IDENT "fwd" ]; t = term ->
         TacticAst.FwdSimpl (loc, t)
-    | [ IDENT "lapply" ]; t = term ->
-        TacticAst.LApply (loc, t)
+    | [ IDENT "lapply" ]; what = tactic_term; 
+        to_what = OPT [ "to" ; t = tactic_term -> t ] ->
+          TacticAst.LApply (loc, to_what, what)
     ]
   ];
   tactical: