- "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 c00eb8404d2f8ca0a459bb28fbca4e0a328f02ac..32625f39f108635b78f3790f5921abdb35738a61 100644 (file)
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -47,16 +47,16 @@ type 'lazy_term reduction =
 type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Absurd of loc * 'term
   | Apply of loc * 'term
+  | ApplyS of loc * 'term
   | Assumption of loc
-  | Auto of loc * int option * int option * string option * string option 
-      (* depth, width, paramodulation, full *) (* ALB *)
+  | Auto of loc * (string * string) list
   | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
-  | Clear of loc * 'ident
+  | Clear of loc * 'ident list
   | ClearBody of loc * 'ident
   | Constructor of loc * int
   | Contradiction of loc
   | Cut of loc * 'ident option * 'term
-  | Decompose of loc * ('term, 'ident) type_spec list * 'ident * 'ident list
+  | Decompose of loc * ('term, 'ident) type_spec list * 'ident option * 'ident list
   | Discriminate of loc * 'term
   | Elim of loc * 'term * 'term option * int option * 'ident list
   | ElimType of loc * 'term * 'term option * int option * 'ident list
@@ -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