?(localise=fun _ -> Stdpp.dummy_loc)
~look_for_coercion metasenv subst context term expty
=
- prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context term);
let force_ty metasenv subst context orig t infty expty =
(*D*)inside 'F'; try let rc =
match expty with
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)
let _, _, arity, cl = List.nth itl tyno in
let constructorsno = List.length cl in
let _, metasenv, args =
- NCicMetaSubst.saturate metasenv context arity 0 in
+ NCicMetaSubst.saturate metasenv subst context arity 0 in
let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in
let metasenv, subst, term, _ =
typeof_aux metasenv subst context (Some ind) term in
| 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 (_,(_,_))
(("_",C.Decl ty_arg) :: context) `Type
in
let flex_prod = C.Prod ("_", ty_arg, meta) in
+ (* next line grants that ty_args is a type *)
+ let metasenv,subst, flex_prod, _ =
+ typeof ~look_for_coercion ~localise metasenv subst
+ context flex_prod None in
pp (lazy ( "UNIFICATION in CTX:\n"^
NCicPp.ppcontext ~metasenv ~subst context
^ "\nOF: " ^