X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCic.ml;h=c4163edb41d9df73ede9068d8ea7cffdbb347a5f;hb=507636cbb473500f40d0969a30e7afc7ddd88f2d;hp=b2f3351c61ed1164b206260e4f4a4d8c8b7ef801;hpb=e43edcc6a209494839326fece1d141f9f189032a;p=helm.git diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index b2f3351c6..c4163edb4 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -13,7 +13,7 @@ (********************************* TERMS ************************************) -type sort = Prop | Set | Type of int | CProp +type sort = Prop | Type of int | CProp type implicit_annotation = [ `Closed | `Type | `Hole | `Term ]