Added initial support for inversion principles in Matita NG.

[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 75e580d00e0cc0c93a93aacb1c35c505783916e6..0480c3d26a53fac04b659530acc2295a622565d6 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 of [`Vector | `JustOne]
+  | Implicit of [`Vector | `JustOne | `Tagged of string]
   | Meta of int * meta_subst list
   | Num of string * int (* literal, instance *)
   | Sort of sort_kind