more comments and compare function for URI exported

diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml
index a9cc9a671f39161afc8500eec4f012d2769fc589..1f02ee7d8e5406c713f32cff20d1e2926699a436 100644 (file)
--- a/helm/software/components/ng_kernel/nCic.ml
+++ b/helm/software/components/ng_kernel/nCic.ml
@@ -47,7 +47,7 @@ type context_entry =                       (* A declaration or definition *)
  | Decl of term                            (* type *)
  | Def  of term * term                     (* body, type *)
 
-type hypothesis = string * context_entry   
+type hypothesis = string * context_entry   (* name, entry *)
 
 type context = hypothesis list
 
@@ -55,7 +55,7 @@ type conjecture = string option * context * term
 
 type metasenv = (int * conjecture) list
 
-type subst_entry = string option * context * term * term
+type subst_entry = string option * context * term * term (* name,ctx,bo,ty *)
 
 type substitution = (int * subst_entry) list
 

diff --git a/helm/software/components/ng_kernel/nUri.mli b/helm/software/components/ng_kernel/nUri.mli
index c5f6333552cb707f15f1f064eb936f70d0dde427..56b49ce88312fdb130fa99ea0bcf03171cf32bbb 100644 (file)
--- a/helm/software/components/ng_kernel/nUri.mli
+++ b/helm/software/components/ng_kernel/nUri.mli
@@ -17,5 +17,7 @@ val string_of_uri: uri -> string
 val name_of_uri: uri -> string
 val uri_of_string: string -> uri
 val eq: uri -> uri -> bool
+val compare: uri -> uri -> int
 
 module UriHash: Hashtbl.S with type key = uri
+