- "linear" flag added to lapply (automatic clearing)

[helm.git] / components / grafite_parser / grafiteParser.ml

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index e9f530f17f49df995ae551ad5f675aef0ec25556..ccff1fab1d3560cd46e2f2a4d3927259418ae747 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -195,12 +195,14 @@ EXTEND
     | IDENT "inversion"; t = tactic_term ->
         GrafiteAst.Inversion (loc, t)
     | IDENT "lapply"; 
+      linear = OPT [ IDENT "linear" ];
       depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
       what = tactic_term; 
       to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
       ident = OPT [ "as" ; ident = IDENT -> ident ] ->
-        let to_what = match to_what with None -> [] | Some to_what -> to_what in
-        GrafiteAst.LApply (loc, depth, to_what, what, ident)
+        let linear = match linear with None -> false | Some _ -> true in 
+       let to_what = match to_what with None -> [] | Some to_what -> to_what in
+        GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
     | IDENT "left" -> GrafiteAst.Left loc
     | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
         GrafiteAst.LetIn (loc, t, where)