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 0480c3d26a53fac04b659530acc2295a622565d6..731a2ba7436f70b6c21f7b05ab0e0274118f9071 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPt.ml
+++ b/helm/software/components/acic_content/cicNotationPt.ml
@@ -94,6 +94,8 @@ type term =
   | Uri of string * subst list option (* as Ident, for long names *)
   | NRef of NReference.reference
 
+  | NCic of NCic.term
+
   (* Syntax pattern extensions *)
 
   | Literal of literal
@@ -177,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