- new syntax for let rec/corec with flavor specifier (tested on lambdadelta/ground_2/)

[helm.git] / matita / components / content / notationPt.ml

diff --git a/matita/components/content/notationPt.ml b/matita/components/content/notationPt.ml
index 731a2ba7436f70b6c21f7b05ab0e0274118f9071..c718a20ba9ebff726ed2556a227dfdfea1df0c92 100644 (file)
--- a/matita/components/content/notationPt.ml
+++ b/matita/components/content/notationPt.ml
@@ -29,8 +29,7 @@
 
 type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
 type induction_kind = [ `Inductive | `CoInductive ]
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of
-CicUniv.universe | `NType of string |`NCProp of string]
+type sort_kind = [ `Prop | `Set | `NType of string |`NCProp of string]
 type fold_kind = [ `Left | `Right ]
 
 type location = Stdpp.location
@@ -38,7 +37,7 @@ let fail floc msg =
   let (x, y) = HExtlib.loc_of_floc floc in
   failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
 
-type href = UriManager.uri
+type href = NReference.reference
 
 type child_pos = [ `Left | `Right | `Inner ]
 
@@ -63,7 +62,7 @@ type 'term capture_variable = 'term * 'term option
 
 (** To be increased each time the term type below changes, used for "safe"
  * marshalling *)
-let magic = 6
+let magic = 8
 
 type term =
   (* CIC AST *)
@@ -77,8 +76,6 @@ type term =
       (* what to match, inductive type, out type, <pattern,action> list *)
   | Cast of term * term
   | LetIn of term capture_variable * term * term  (* name, body, where *)
-  | LetRec of induction_kind * (term capture_variable list * term capture_variable * term * int) list * term
-      (* (params, name, body, decreasing arg) list, where *)
   | Ident of string * subst list option
       (* literal, substitutions.
       * Some [] -> user has given an empty explicit substitution list 
@@ -166,7 +163,6 @@ type argument_pattern =
   | IdentArg of int * string (* eta-depth, name *)
 
 type cic_appl_pattern =
-  | UriPattern of UriManager.uri
   | NRefPattern of NReference.reference
   | VarPattern of string
   | ImplicitPattern
@@ -177,18 +173,20 @@ type cic_appl_pattern =
 type 'term inductive_type = string * bool * 'term * (string * 'term) list
 
 type 'term obj =
-  | Inductive of 'term capture_variable list * 'term inductive_type list
+  | Inductive of 'term capture_variable list * 'term inductive_type list * NCic.source
       (** parameters, list of loc * mutual inductive types *)
-  | Theorem of Cic.object_flavour * string * 'term * 'term option * NCic.def_pragma
-      (** flavour, name, type, body
+  | Theorem of string * 'term * 'term option * NCic.c_attr
+      (** name, type, body, attributes
        * - name is absent when an unnamed theorem is being proved, tipically in
        *   interactive usage
        * - body is present when its given along with the command, otherwise it
        *   will be given in proof editing mode using the tactical language,
        *   unless the flavour is an Axiom
        *)
-  | Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list
+  | Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list * NCic.source
       (** left parameters, name, type, fields *)
+  | LetRec of induction_kind * ('term capture_variable list * 'term capture_variable * 'term * int) list * NCic.f_attr
+      (* (params, name, body, decreasing arg) list, attributes *)
 
 (** {2 Standard precedences} *)
 
@@ -196,4 +194,3 @@ let let_in_prec = 10
 let binder_prec = 20
 let apply_prec = 70
 let simple_prec = 90
-