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

[helm.git] / components / grafite / grafiteAst.ml

diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index c73657ae1b4f8c458e5d290e5a202b15db41f7c0..32625f39f108635b78f3790f5921abdb35738a61 100644 (file)
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -72,7 +72,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Injection of loc * 'term
   | Intros of loc * int option * 'ident list
   | Inversion of loc * 'term
-  | LApply of loc * int option * 'term list * 'term * 'ident option
+  | LApply of loc * bool * int option * 'term list * 'term * 'ident option
   | Left of loc
   | LetIn of loc * 'term * 'ident
   | Reduce of loc * 'reduction * ('term, 'lazy_term, 'ident) pattern