From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 9 Dec 2008 18:29:37 +0000 (+0000)
Subject: raise uncertain when a sort is not a sort but may be, use max for mixing universes... 
X-Git-Tag: make_still_working~4424
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=63e7ef727ce32552106c4d8f3030fd264532fffe;p=helm.git

raise uncertain when a sort is not a sort but may be, use max for mixing universes, coercions to sort in the prod case are triggered before putting the source type in the context
---

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 191bd708c..72a6409ef 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -162,8 +162,14 @@ let rec typeof
        metasenv, subst, t, NCicTypeChecker.typeof ~subst ~metasenv context t
     | C.Prod (name,(s as orig_s),(t as orig_t)) ->
        let metasenv, subst, s, s1 = typeof_aux metasenv subst context None s in
+       let metasenv, subst, s, s1 = 
+         force_to_sort ~look_for_coercion
+           metasenv subst context s orig_s localise s1 in
        let context1 = (name,(C.Decl s))::context in
        let metasenv, subst, t, s2 = typeof_aux metasenv subst context1 None t in
+       let metasenv, subst, t, s2 = 
+         force_to_sort ~look_for_coercion
+           metasenv subst context1 t orig_t localise s2 in
        let metasenv, subst, s, t, ty = 
          sort_of_prod ~look_for_coercion localise metasenv subst 
            context orig_s orig_t (name,s) t (s1,s2)
@@ -330,23 +336,18 @@ and force_to_sort
   | ty -> 
       try_coercions ~localise ~look_for_coercion metasenv subst context
         t orig_t ty (NCic.Sort (NCic.Type NCicEnvironment.type0)) false 
-         (RefineFailure (lazy (localise orig_t, 
+         (Uncertain (lazy (localise orig_t, 
          "The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t
          ^ " is not a sort: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty)))
 
 and sort_of_prod ~look_for_coercion
   localise metasenv subst context orig_s orig_t (name,s) t (t1, t2) 
 =
-   let metasenv, subst, s, t1 = 
-     force_to_sort 
-      ~look_for_coercion metasenv subst context s orig_s localise t1 in
-   let metasenv, subst, t, t2 = 
-     force_to_sort ~look_for_coercion metasenv subst ((name,C.Decl s)::context) 
-       t orig_t localise t2 in
+   (* force to sort is done in the Prod case in typeof *)
    match t1, t2 with
    | C.Sort _, C.Sort C.Prop -> metasenv, subst, s, t, t2
    | C.Sort (C.Type u1), C.Sort (C.Type u2) ->
-        metasenv, subst, s, t, C.Sort (C.Type (u1@u2)) 
+        metasenv, subst, s, t, C.Sort (C.Type (NCicEnvironment.max u1 u2)) 
    | C.Sort C.Prop,C.Sort (C.Type _) -> metasenv, subst, s, t, t2
    | C.Meta _, C.Sort _ 
    | C.Meta _, C.Meta (_,(_,_))