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

[helm.git] / components / grafite_engine / grafiteEngine.ml

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index 52dde8979f72381e0c7d0297dd8628bc69f29632..d7343c98c1447c5831ace4066798c6828e37fd09 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -130,10 +130,10 @@ let tactic_of_ast ast =
         ~mk_fresh_name_callback:(namer_of names) ()
   | GrafiteAst.Inversion (_, term) ->
       Tactics.inversion term
-  | GrafiteAst.LApply (_, how_many, to_what, what, ident) ->
+  | GrafiteAst.LApply (_, linear, how_many, to_what, what, ident) ->
       let names = match ident with None -> [] | Some id -> [id] in
-      Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many
-        ~to_what what
+      Tactics.lapply ~mk_fresh_name_callback:(namer_of names) 
+        ~linear ?how_many ~to_what what
   | GrafiteAst.Left _ -> Tactics.left
   | GrafiteAst.LetIn (loc,term,name) ->
       Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])