CProp hierarchy is there!

[helm.git] / helm / software / components / cic_unification / cicRefine.ml

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 04d9d7224d6430a274e300d94bc59bde2b295b7f..b5204de02f78baa2a6731d25c5e61bfe7aa11cef 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -801,7 +801,8 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                         in
                           C.Appl (outtype'::args)
                       in
-                        CicReduction.whd ~subst context appl
+                        CicReduction.head_beta_reduce ~delta:false 
+                          ~upto:(List.length args) appl 
                     in
                      try
                       fo_unif_subst subst context metasenv instance instance'
@@ -1064,8 +1065,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
     let t1'' = CicReduction.whd ~subst context t1 in
     let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
       match (t1'', t2'') with
-          (C.Sort s1, C.Sort s2)
-            when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> 
+        | (C.Sort s1, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) -> 
               (* different than Coq manual!!! *)
               C.Sort s2,subst,metasenv,ugraph
         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
@@ -1076,8 +1076,34 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                 C.Sort (C.Type t'),subst,metasenv,ugraph2
               with
                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+        | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) -> 
+            let t' = CicUniv.fresh() in 
+             (try
+              let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+              let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+                C.Sort (C.CProp t'),subst,metasenv,ugraph2
+              with
+               CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+        | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) -> 
+            let t' = CicUniv.fresh() in 
+             (try
+              let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+              let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+                C.Sort (C.CProp t'),subst,metasenv,ugraph2
+              with
+               CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+        | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) -> 
+            let t' = CicUniv.fresh() in 
+             (try
+              let ugraph1 = CicUniv.add_gt t' t1 ugraph in
+              let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+                C.Sort (C.Type t'),subst,metasenv,ugraph2
+              with
+               CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
         | (C.Sort _,C.Sort (C.Type t1)) -> 
             C.Sort (C.Type t1),subst,metasenv,ugraph
+        | (C.Sort _,C.Sort (C.CProp t1)) -> 
+            C.Sort (C.CProp t1),subst,metasenv,ugraph
         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
         | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
             (* TODO how can we force the meta to become a sort? If we don't we