| (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 ugraph1 = CicUniv.add_ge t' t1 ugraph in
let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
C.Sort (C.Type t'),subst,metasenv,ugraph2
with
(* given he:hety, gives beack all (c he) such that (c e):?->? *)
let fix_arity n metasenv context subst he hetype ugraph =
let hetype = CicMetaSubst.apply_subst subst hetype in
- let src = CoercDb.coerc_carr_of_term hetype 0 in
- let tgt = CoercDb.coerc_carr_of_term (Cic.Implicit None) 1 in
- match CoercGraph.look_for_coercion' metasenv subst context src tgt with
+ (* instead of a dummy functional type we may create the real product
+ * using args_bo_and_ty, but since coercions lookup ignores the
+ * actual ariety we opt for the simple solution *)
+ let fty = Cic.Prod(Cic.Anonymous, Cic.Sort Cic.Prop, Cic.Sort Cic.Prop) in
+ match CoercGraph.look_for_coercion metasenv subst context hetype fty with
| CoercGraph.NoCoercion -> []
| CoercGraph.NotHandled ->
raise (MoreArgsThanExpected (n,Uncertain (lazy "")))