From d030f02fa8a708cd663ffd0c5783770906b9b21a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 1 Apr 2008 08:59:02 +0000
Subject: [PATCH] added some comments, but the samentics of many functions is
 still unclear to me

---
 helm/software/components/tactics/universe.ml  |  2 +-
 helm/software/components/tactics/universe.mli | 24 ++++++++++++++-----
 2 files changed, 19 insertions(+), 7 deletions(-)

diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml
index 6a0a31566..c4e439efe 100644
--- a/helm/software/components/tactics/universe.ml
+++ b/helm/software/components/tactics/universe.ml
@@ -120,7 +120,7 @@ let keys context ty =
     [head true ty; head true (unfold context ty)]
   with ProofEngineTypes.Fail _ -> [head true ty]
 
-let key term = head false term
+let key term = head false term;;
 
 let index_term_and_unfolded_term univ context t ty =
   let key = head true ty in
diff --git a/helm/software/components/tactics/universe.mli b/helm/software/components/tactics/universe.mli
index 9201d92b8..de7c20871 100644
--- a/helm/software/components/tactics/universe.mli
+++ b/helm/software/components/tactics/universe.mli
@@ -24,19 +24,31 @@
  *)
 
 type universe
+
 val empty : universe
+
+(* retrieves the list of term that hopefully unify *)
 val get_candidates: universe -> Cic.term -> Cic.term list
-val index:
-  universe -> 
-  Cic.term -> (* key *)
-  Cic.term -> (* value *)
-  universe
+
+(* index [univ] [key] [term] *)
+val index: universe -> Cic.term -> Cic.term -> universe
+
+(* collapse non-indexable terms, removing coercions an unfolding the head
+ * constant if any *)
 val keys: Cic.context -> Cic.term -> Cic.term list
-val key: Cic.term -> Cic.term
+
+(* collapse non-indexable terms, not removing coercions *)
+val key: Cic.term -> Cic.term 
+
+(* indexes the term and its unfolded both without coercions *)
 val index_term_and_unfolded_term: 
   universe -> Cic.context -> Cic.term -> Cic.term -> universe
+
+(* indexex the term without coercions, with coercions and unfolded without
+ * coercions *)
 val index_local_term: 
   universe -> Cic.context -> Cic.term -> Cic.term -> universe
+
 (* pairs are (term,ty) *)
 val index_list: 
     universe -> Cic.context -> (Cic.term*Cic.term) list -> universe
-- 
2.39.2