X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCic.ml;h=e520422160ab7fc77a41069b3970b960c4b2ca6d;hb=a03741c70a531bdfcc97eddca21e30eb3cd82073;hp=97733891e8745b4e3251500878f4804abe1743ef;hpb=c14ddc094a1cfa93b5337e5aecc6831f72dfc22b;p=helm.git

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