Partially restore the suppose tactic

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

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index 2d55e8634fd73bd88b44ee9ede5ae07e158ad84e..29dfe324b4426e25ade914f6aa5aac0be7f65677 100644 (file)
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -75,6 +75,10 @@ type ntactic =
    | NAssumption of loc
    | NRepeat of loc * ntactic
    | NBlock of loc * ntactic list
+   (* Declarative langauge *)
+   (* Not the best idea to use a string directly, an abstract type for identifiers would be better *)
+   | Assume of loc * string * nterm (* loc, identifier, term *)
+   | Suppose of loc * nterm *string * nterm option
 
 type nmacro =
   | NCheck of loc * nterm
@@ -84,7 +88,7 @@ type nmacro =
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 36
+let magic = 37
 
 (* composed magic: term + command magics. No need to change this value *)
 let magic = magic + 10000 * NotationPt.magic
@@ -99,10 +103,10 @@ type inclusion_mode = WithPreferences | WithoutPreferences | OnlyPreferences (*
 type command =
   | Include of loc * inclusion_mode * string (* _,buri,_,path *)
   | UnificationHint of loc * nterm * int (* term, precedence *)
-  | NObj of loc * nterm NotationPt.obj
+  | NObj of loc * nterm NotationPt.obj * bool
   | NDiscriminator of loc * nterm
   | NInverter of loc * string * nterm * bool list option * nterm option
-  | NUnivConstraint of loc * NUri.uri * NUri.uri
+  | NUnivConstraint of loc * bool * NUri.uri * NUri.uri
   | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
   | NCoercion of loc * string * bool * 
       (nterm * nterm * (string * nterm) * nterm) option