| (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 "")))
"Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
"\n but is applyed to: " ^ String.concat ";"
(List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
+ let error = ref None in
let possible_fixes =
fix_arity (List.length args) metasenv context subst he hetype
ugraph in
with
| RefineFailure _ | Uncertain _
| HExtlib.Localized (_,RefineFailure _)
- | HExtlib.Localized (_,Uncertain _) -> None)
+ | HExtlib.Localized (_,Uncertain _) as exn ->
+ error := Some exn; None)
possible_fixes
with
| Some x -> x
| None ->
- raise
- (MoreArgsThanExpected
- (List.length args, RefineFailure (lazy "")))
+ match !error with
+ None ->
+ raise
+ (MoreArgsThanExpected
+ (List.length args, RefineFailure (lazy "")))
+ | Some exn -> raise exn
in
(* first we check if we are in the simple case of a meta closed term *)
let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =