X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=87b3f7f42a319f227f06ce9d9c7b3db5bfc85e53;hb=1bbc2dd649df75e33f2cd7fb3e5ecb15f526a442;hp=a1a7bdea8ebe9f5861bb602d61fd13cf7e390abe;hpb=ab8e7d8565ef3840362bc3913e1a01f4824ee209;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index a1a7bdea8..87b3f7f42 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1065,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)) -> 
@@ -1077,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
@@ -1598,11 +1623,12 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                      CicTypeChecker.type_of_aux' ~subst metasenv context m
                        CicUniv.oblivion_ugraph 
                    with
-                   | Cic.MutInd _ as mty,_ -> [], mty
-                   | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
+                   | (Cic.MutInd _ | Cic.Meta _) as mty,_ -> [], mty
+                   | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ ->
                        snd (HExtlib.split_nth leftno args), mty
                    | _ -> assert false
-                 with CicTypeChecker.TypeCheckerFailure _ -> assert false
+                 with CicTypeChecker.TypeCheckerFailure _ -> 
+                    raise (AssertFailure(lazy "already ill-typed matched term"))
                in
                let new_outty =
                 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)