Type of conjecture and subst_entry made uniform.

[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..c2e1c53d2d36cad3c6ccb022c0118fbb9e5d3871 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 ]
 
@@ -47,9 +47,9 @@ type hypothesis = string * context_entry
 
 type context = hypothesis list
 
-type conjecture = int * string option * context * term
+type conjecture = string option * context * term
 
-type metasenv = conjecture list
+type metasenv = (int * conjecture) list
 
 type subst_entry = string option * context * term * term
 
@@ -60,6 +60,7 @@ type substitution = (int * subst_entry) list
 
 type relevance = bool list (* relevance of arguments for conversion *)
 
+                    (* relevance, name, recno, ty, bo *)
 type inductiveFun = relevance * string * int * term * term 
   (* if coinductive, the int has no meaning and must be set to -1 *)