From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 19 Sep 2008 07:57:25 +0000 (+0000)
Subject: more comments and compare function for URI exported
X-Git-Tag: make_still_working~4763
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7954b6bd597d7999392bf9fe8d02b7c94f71925f;p=helm.git

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 a9cc9a671..1f02ee7d8 100644
--- 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 c5f633355..56b49ce88 100644
--- 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
+