1) The NG kernel now accepts only usage of declared universes

2) Bug (badly) fixed in NCicElim: it used to generate undeclared universe
   names.

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 07185a9476eb61b7b508f397b34a518ee45d5cc8..b3b1eda16eab228c19944d7f7f176e2ffd6433e9 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -77,6 +77,12 @@ let universes = ref [];;
 
 let get_universes () = List.map (fun x -> [false,x]) !universes;;
 
+let is_declared u =
+ match u with
+    [false,x] -> List.exists (fun y -> NUri.eq x y) !universes
+  | _ -> assert false
+;;
+
 let add_constraint strict a b = 
   match a,b with
   | [false,a2],[false,b2] -> 

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli
index 0e0fe48451c7b3f7ec70cfe7e9879cebec6f80b4..778931706e3fa828abd40e2d62753e19426c1944 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.mli
+++ b/helm/software/components/ng_kernel/nCicEnvironment.mli
@@ -27,6 +27,7 @@ val get_relevance: NReference.reference -> bool list
 
 val type0: NCic.universe
 val get_universes: unit -> NCic.universe list
+val is_declared: NCic.universe -> bool
 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

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index c19561d355821bfffa6fa7fceffeb11ef0a299cd..695b2e5319f61df33cdd05115c4058c2cf94adbd 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -391,7 +391,12 @@ let rec typeof ~subst ~metasenv context term =
         with Failure _ -> 
           raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n
             ^" under: " ^ NCicPp.ppcontext ~metasenv ~subst context))))
-    | C.Sort (C.Type [false,u]) -> C.Sort (C.Type [true, u])
+    | C.Sort (C.Type ([false,u] as univ)) ->
+       if NCicEnvironment.is_declared univ then
+        C.Sort (C.Type [true, u])
+       else
+        raise (TypeCheckerFailure (lazy ("undeclared universe " ^
+         NUri.string_of_uri u)))
     | C.Sort (C.Type _) -> 
         raise (AssertFailure (lazy ("Cannot type an inferred type: "^
           NCicPp.ppterm ~subst ~metasenv ~context t)))

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index ae472ae38cbdaf37633b73fe2655342d589fa1bc..ef33ceeab20cf6c1d7c1fb3aab65091fe0fd11ed 100644 (file)
--- a/helm/software/components/ng_tactics/nCicElim.ml
+++ b/helm/software/components/ng_tactics/nCicElim.ml
@@ -157,7 +157,15 @@ let mk_elims (uri,_,_,_,obj) =
       NCic.Prop -> `Prop,"ind"
     | NCic.Type u ->
        let u = NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] (NCic.Sort s) in
-       `NType u, "rect_" ^ u
+       (try
+         if String.sub u 0 4 = "Type" then
+          `NType (String.sub u 4 (String.length u - 4)), "rect_" ^ u
+         else if String.sub u 0 5 = "CProp" then
+          `NCProp (String.sub u 5 (String.length u - 5)), "rect_" ^ u
+         else
+          (prerr_endline u;
+          assert false)
+        with Failure _ -> assert false)
  in
   match obj with
      NCic.Inductive (true,leftno,itl,_) ->