X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=ccff1fab1d3560cd46e2f2a4d3927259418ae747;hb=e31bb143e3a303321e509f415764338849b7e516;hp=e9f530f17f49df995ae551ad5f675aef0ec25556;hpb=cc3ab906b631ef0edb4402cb622fc3fa96682717;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index e9f530f17..ccff1fab1 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/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)