Use seed to avoid further name clashes.

[helm.git] / helm / software / components / ng_kernel / nCic.ml

diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml
index b2f3351c61ed1164b206260e4f4a4d8c8b7ef801..c4163edb41d9df73ede9068d8ea7cffdbb347a5f 100644 (file)
--- 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 ]