From 1f0e9fc3bf85b8a7aa0876051bf4788252a41f44 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 16 Sep 2008 10:23:35 +0000
Subject: [PATCH] ...

---
 helm/software/components/ng_refiner/.depend           |  2 ++
 helm/software/components/ng_refiner/.depend.opt       |  2 ++
 ...{discrimination_tree.ml => nDiscriminationTree.ml} | 11 ++++-------
 ...iscrimination_tree.mli => nDiscriminationTree.mli} | 10 +++++-----
 4 files changed, 13 insertions(+), 12 deletions(-)
 rename helm/software/components/ng_refiner/{discrimination_tree.ml => nDiscriminationTree.ml} (95%)
 rename helm/software/components/ng_refiner/{discrimination_tree.mli => nDiscriminationTree.mli} (74%)

diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend
index 1bedd90f6..b71e499a1 100644
--- a/helm/software/components/ng_refiner/.depend
+++ b/helm/software/components/ng_refiner/.depend
@@ -1,3 +1,5 @@
+nDiscriminationTree.cmo: nDiscriminationTree.cmi 
+nDiscriminationTree.cmx: nDiscriminationTree.cmi 
 nCicMetaSubst.cmo: nCicMetaSubst.cmi 
 nCicMetaSubst.cmx: nCicMetaSubst.cmi 
 nCicUnification.cmo: nCicUnification.cmi 
diff --git a/helm/software/components/ng_refiner/.depend.opt b/helm/software/components/ng_refiner/.depend.opt
index 1bedd90f6..b71e499a1 100644
--- a/helm/software/components/ng_refiner/.depend.opt
+++ b/helm/software/components/ng_refiner/.depend.opt
@@ -1,3 +1,5 @@
+nDiscriminationTree.cmo: nDiscriminationTree.cmi 
+nDiscriminationTree.cmx: nDiscriminationTree.cmi 
 nCicMetaSubst.cmo: nCicMetaSubst.cmi 
 nCicMetaSubst.cmx: nCicMetaSubst.cmi 
 nCicUnification.cmo: nCicUnification.cmi 
diff --git a/helm/software/components/ng_refiner/discrimination_tree.ml b/helm/software/components/ng_refiner/nDiscriminationTree.ml
similarity index 95%
rename from helm/software/components/ng_refiner/discrimination_tree.ml
rename to helm/software/components/ng_refiner/nDiscriminationTree.ml
index 01d7136ea..1089474e4 100644
--- a/helm/software/components/ng_refiner/discrimination_tree.ml
+++ b/helm/software/components/ng_refiner/nDiscriminationTree.ml
@@ -38,14 +38,11 @@ module DiscriminationTreeIndexing =
         | NCic.Rel i -> Bound i
         | NCic.Sort (NCic.Prop) -> Proposition
         | NCic.Sort _ -> Datatype
-        | NCic.Const _ | NCic.Var _ | NCic.MutInd _ | NCic.MutConstruct _ as t ->
-            (try Constant (CicUtil.uri_of_term t)
-            with Invalid_argument _ -> assert false)
+        | NCic.Const (NReference.Ref (u,_)) -> Constant u
         | NCic.Appl _ -> 
             assert false (* should not happen *)
-        | NCic.LetIn _ | NCic.Lambda _ | NCic.Prod _ | NCic.Cast _
-        | NCic.MutCase _ | NCic.Fix _ | NCic.CoFix _ -> 
-            HLog.debug "FIXME: the trie receives an invalid term";
+        | NCic.LetIn _ | NCic.Lambda _ | NCic.Prod _ | NCic.Match _ -> 
+            prerr_endline "FIXME: the discrimination tree receives an invalid term";
             Dead
             (* assert false universe.ml removes these *)
       ;;
@@ -69,7 +66,7 @@ module DiscriminationTreeIndexing =
       ;;
       let compare_elem e1 e2 =
         match e1,e2 with
-        | Constant u1,Constant u2 -> NUri.compare u1 u2
+        | Constant u1,Constant u2 -> assert false (*NUri.compare u1 u2*)
         | e1,e2 -> Pervasives.compare e1 e2
       ;;
 
diff --git a/helm/software/components/ng_refiner/discrimination_tree.mli b/helm/software/components/ng_refiner/nDiscriminationTree.mli
similarity index 74%
rename from helm/software/components/ng_refiner/discrimination_tree.mli
rename to helm/software/components/ng_refiner/nDiscriminationTree.mli
index 896e264cd..a146c4b73 100644
--- a/helm/software/components/ng_refiner/discrimination_tree.mli
+++ b/helm/software/components/ng_refiner/nDiscriminationTree.mli
@@ -20,11 +20,11 @@ module DiscriminationTreeIndexing :
       val iter : t -> (A.t -> unit) -> unit
 
       val empty : t
-      val index : t -> Cic.term -> A.elt -> t
-      val remove_index : t -> Cic.term -> A.elt -> t
-      val in_index : t -> Cic.term -> (A.elt -> bool) -> bool
-      val retrieve_generalizations : t -> Cic.term -> A.t
-      val retrieve_unifiables : t -> Cic.term -> A.t
+      val index : t -> NCic.term -> A.elt -> t
+      val remove_index : t -> NCic.term -> A.elt -> t
+      val in_index : t -> NCic.term -> (A.elt -> bool) -> bool
+      val retrieve_generalizations : t -> NCic.term -> A.t
+      val retrieve_unifiables : t -> NCic.term -> A.t
     end
 
 
-- 
2.39.2