made executable again

[helm.git] / helm / software / components / acic_content / cicNotationPt.ml

diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml
index 46381e4bc505ea6608fc4548af9cf8aec88f1863..731a2ba7436f70b6c21f7b05ab0e0274118f9071 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPt.ml
+++ b/helm/software/components/acic_content/cicNotationPt.ml
@@ -83,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
@@ -92,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 *)
 
@@ -164,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
@@ -175,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