From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 29 Apr 2005 18:52:57 +0000 (+0000)
Subject: added more assertions on universes when loaded from dump (and fixed some bugs concern... 
X-Git-Tag: single_binding~127
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d450cacb49707a71fe93489a1bf64db4689612d6;p=helm.git

added more assertions on universes when loaded from dump (and fixed some bugs concerning re-hash-consing)
---

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 08166d564..367336f7f 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -165,6 +165,9 @@ module Cache :
               ) l
             in
              C.Meta(i,l')
+         | C.Sort (C.Type u) -> 
+             CicUniv.assert_univ u;
+             C.Sort (C.Type (CicUniv.recons_univ u))
          | C.Sort _ as t -> t
          | C.Implicit _ as t -> t
          | C.Cast (te,ty) -> C.Cast (restore_in_term te, restore_in_term ty)
@@ -214,7 +217,7 @@ module Cache :
             in
              C.CoFix (i, liftedfl)
       in
-      function
+      function 
          C.Constant (name,bo,ty,params,attrs) ->
            let bo' =
              match bo with
diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index abb1b86f3..b8ae1602c 100644
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -85,7 +85,8 @@ let rec pp t l =
        (match s with
            C.Prop  -> "Prop"
          | C.Set   -> "Set"
-         | C.Type _ -> "Type" (* TASSI: universe is not explicit *)
+         | C.Type _ -> "Type"
+         (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
 	 | C.CProp -> "CProp" 
        )
     | C.Implicit _ -> "?"