Fixed (yet another) nasty bug, in deep_eq this time

[helm.git] / helm / software / components / cic_proof_checking / cicUnivUtils.ml

diff --git a/helm/software/components/cic_proof_checking/cicUnivUtils.ml b/helm/software/components/cic_proof_checking/cicUnivUtils.ml
index 948b26ff0bf62e372648f8ab175112cd0b455d9a..2c35ebe1a05badb17fd5269edfa4411662bb5c2e 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicUnivUtils.ml
+++ b/helm/software/components/cic_proof_checking/cicUnivUtils.ml
@@ -79,6 +79,8 @@ let universes_of_obj uri t =
     | C.Meta (n,l1) -> C.Meta (n, List.map (HExtlib.map_option aux) l1)
     | C.Sort (C.Type i) -> add_result [i]; 
       C.Sort (C.Type (CicUniv.name_universe i uri))
+    | C.Sort (C.CProp i) -> add_result [i]; 
+      C.Sort (C.CProp (CicUniv.name_universe i uri))
     | C.Rel _ 
     | C.Sort _
     | C.Implicit _ as x -> x