From d450cacb49707a71fe93489a1bf64db4689612d6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 29 Apr 2005 18:52:57 +0000 Subject: [PATCH] added more assertions on universes when loaded from dump (and fixed some bugs concerning re-hash-consing) --- helm/ocaml/cic_proof_checking/cicEnvironment.ml | 5 ++++- helm/ocaml/cic_proof_checking/cicPp.ml | 3 ++- 2 files changed, 6 insertions(+), 2 deletions(-) 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 _ -> "?" -- 2.39.2