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

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

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 16421efafb386df29236fe77b36e9a9ba05b0cfe..5babe3604b2478424cfc48c0ed27e5432a3ee0fb 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -212,14 +212,14 @@ let disambiguate_tactic
     | GrafiteAst.Inversion (loc, term) ->
        let metasenv,term = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Inversion (loc, term)
-    | GrafiteAst.LApply (loc, depth, to_what, what, ident) ->
+    | GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) ->
        let f term to_what =
           let metasenv,term = disambiguate_term context metasenv term in
           term :: to_what
        in
        let to_what = List.fold_right f to_what [] in 
        let metasenv,what = disambiguate_term context metasenv what in
-       metasenv,GrafiteAst.LApply (loc, depth, to_what, what, ident)
+       metasenv,GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
     | GrafiteAst.Left loc ->
        metasenv,GrafiteAst.Left loc
     | GrafiteAst.LetIn (loc, term, name) ->