X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPt.ml;h=0480c3d26a53fac04b659530acc2295a622565d6;hb=ddd6560f4e70ec3306d223738a441d5f1dd3eac9;hp=75e580d00e0cc0c93a93aacb1c35c505783916e6;hpb=7ca0a000878e864c92d94f77900bc2ca0ac143b9;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml
index 75e580d00..0480c3d26 100644
--- 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