1) added a function to retrieve all the universes currently in use

2) INCONSISTENCY BUG FIXED: it was possible to _redefine_ an already defined
   constant. Thus it was very easy to prove False!

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 78abb68019f37a9f5aa7d9aa8a91cd7087f80071..07185a9476eb61b7b508f397b34a518ee45d5cc8 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -18,6 +18,7 @@ exception CircularDependency of string Lazy.t;;
 exception ObjectNotFound of string Lazy.t;;
 exception BadDependency of string Lazy.t * exn;;
 exception BadConstraint of string Lazy.t;;
+exception AlreadyDefined of string Lazy.t;;
 
 let cache = NUri.UriHash.create 313;;
 let history = ref [];;
@@ -74,6 +75,8 @@ let pp_constraints () =
 
 let universes = ref [];;
 
+let get_universes () = List.map (fun x -> [false,x]) !universes;;
+
 let add_constraint strict a b = 
   match a,b with
   | [false,a2],[false,b2] -> 
@@ -199,7 +202,12 @@ let get_checked_obj u =
 
 let get_checked_obj u = to_exn get_checked_obj u;;
 
-let check_and_add_obj obj = ignore (to_exn check_and_add_obj obj);;
+let check_and_add_obj ((u,_,_,_,_) as obj) =
+ if NUri.UriHash.mem cache u then
+  raise (AlreadyDefined (lazy (NUri.string_of_uri u)))
+ else
+  ignore (to_exn check_and_add_obj obj)
+;;
 
 let get_checked_decl = function
   | Ref.Ref (uri, Ref.Decl) ->

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli
index 5252ddb8b5f271bd307cd36d4590b8dd8a0e91c2..0e0fe48451c7b3f7ec70cfe7e9879cebec6f80b4 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.mli
+++ b/helm/software/components/ng_kernel/nCicEnvironment.mli
@@ -15,6 +15,7 @@ exception CircularDependency of string Lazy.t;;
 exception ObjectNotFound of string Lazy.t;;
 exception BadDependency of string Lazy.t * exn;;
 exception BadConstraint of string Lazy.t;;
+exception AlreadyDefined of string Lazy.t;;
 
 val set_get_obj: (NUri.uri -> NCic.obj) -> unit
 
@@ -25,6 +26,7 @@ val check_and_add_obj: NCic.obj -> unit
 val get_relevance: NReference.reference -> bool list
 
 val type0: NCic.universe
+val get_universes: unit -> NCic.universe list
 val max: NCic.universe -> NCic.universe -> NCic.universe
 (* universe_* raise BadConstraints if the second arg. is an inferred universe *)
 val universe_eq: NCic.universe -> NCic.universe -> bool