X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCic.ml;h=fead92210f45053b925c7acbc82aeb6f55b64cce;hb=ddd6560f4e70ec3306d223738a441d5f1dd3eac9;hp=f39cf868e32fe905a123e4c8b3f516d67e4a68f7;hpb=7ca0a000878e864c92d94f77900bc2ca0ac143b9;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml
index f39cf868e..fead92210 100644
--- a/helm/software/components/ng_kernel/nCic.ml
+++ b/helm/software/components/ng_kernel/nCic.ml
@@ -22,7 +22,8 @@ type universe = (univ_algebra * NUri.uri) list
 type sort = Prop | Type of universe
 
 type implicit_annotation =
- [ `Closed | `Type | `Hole | `Term | `Typeof of int | `Vector ]
+ [ `Closed | `Type | `Hole | `Tagged of string | `Term | `Typeof of int | `Vector ]
+
 
 type lc_kind = Irl of int | Ctx of term list