X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPt.ml;h=731a2ba7436f70b6c21f7b05ab0e0274118f9071;hb=4a747f4352bd5961c60a7d75eaa95ac3ee4f54f9;hp=cfbd21b3a7f0c61f48e07e97dcdd8993ec53b6f7;hpb=be73a507f4f3c1b40a77dd7fc587adaf45b4d8ea;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml
index cfbd21b3a..731a2ba74 100644
--- a/helm/software/components/acic_content/cicNotationPt.ml
+++ b/helm/software/components/acic_content/cicNotationPt.ml
@@ -29,7 +29,8 @@
 
 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]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of
+CicUniv.universe | `NType of string |`NCProp of string]
 type fold_kind = [ `Left | `Right ]
 
 type location = Stdpp.location
@@ -82,7 +83,7 @@ type term =
       (* literal, substitutions.
       * Some [] -> user has given an empty explicit substitution list 
       * None -> user has given no explicit substitution list *)
-  | Implicit
+  | Implicit of [`Vector | `JustOne | `Tagged of string]
   | Meta of int * meta_subst list
   | Num of string * int (* literal, instance *)
   | Sort of sort_kind
@@ -91,6 +92,9 @@ type term =
   | UserInput (* place holder for user input, used by MatitaConsole, not to be
               used elsewhere *)
   | Uri of string * subst list option (* as Ident, for long names *)
+  | NRef of NReference.reference
+
+  | NCic of NCic.term
 
   (* Syntax pattern extensions *)
 
@@ -122,6 +126,7 @@ and layout_pattern =
   | InfRule of term * term * term
 (*   | array of term * literal option * literal option
       |+ column separator, row separator +| *)
+  | Maction of term list
   | Sqrt of term
   | Root of term * term (* argument, index *)
   | Break
@@ -162,6 +167,7 @@ type argument_pattern =
 
 type cic_appl_pattern =
   | UriPattern of UriManager.uri
+  | NRefPattern of NReference.reference
   | VarPattern of string
   | ImplicitPattern
   | ApplPattern of cic_appl_pattern list
@@ -173,7 +179,7 @@ type 'term inductive_type = string * bool * 'term * (string * 'term) list
 type 'term obj =
   | Inductive of 'term capture_variable list * 'term inductive_type list
       (** parameters, list of loc * mutual inductive types *)
-  | Theorem of Cic.object_flavour * string * 'term * 'term option
+  | Theorem of Cic.object_flavour * string * 'term * 'term option * NCic.def_pragma
       (** flavour, name, type, body
        * - name is absent when an unnamed theorem is being proved, tipically in
        *   interactive usage