From aa130b53c16a58c29f017510d876a31b674a2504 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 4 Oct 2012 22:08:08 +0000 Subject: Improving error message when abtraction over goal (abstract_list_all used when applying schemes - induction, rewrite, ...) is well-typed but not of the right type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15853 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/unification.ml | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) (limited to 'pretyping/unification.ml') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 886c4a3aa..e25a880f8 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -60,15 +60,17 @@ let abstract_scheme env c l lname_typ = (List.rev l) lname_typ +(* Precondition: resulting abstraction is expected to be of type [typ] *) + let abstract_list_all env evd typ c l = let ctxt,_ = splay_prod_n env evd (List.length l) typ in let l_with_all_occs = List.map (function a -> (AllOccurrences,a)) l in let p = abstract_scheme env c l_with_all_occs ctxt in - try - if is_conv_leq env evd (Typing.type_of env evd p) typ then p - else error "abstract_list_all" - with UserError _ | Type_errors.TypeError _ -> - error_cannot_find_well_typed_abstraction env evd p l + let typp = + try Typing.type_of env evd p + with UserError _ | Type_errors.TypeError _ -> + error_cannot_find_well_typed_abstraction env evd p l in + (p,typp) let set_occurrences_of_last_arg args = Some AllOccurrences :: List.tl (Array.map_to_list (fun _ -> None) args) @@ -1176,7 +1178,10 @@ let secondOrderAbstraction env evd flags typ (p, oplist) = let flags = { flags with modulo_delta = (fst flags.modulo_delta, Cpred.empty) } in let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in let typp = Typing.meta_type evd' p in - let pred = abstract_list_all env evd' typp typ cllist in + let pred,predtyp = abstract_list_all env evd' typp typ cllist in + if not (is_conv_leq env evd predtyp typp) then + error_wrong_abstraction_type env evd + (Evd.meta_name evd p) pred typp predtyp; w_merge env false flags (evd',[p,pred,(Conv,TypeProcessed)],[]) let secondOrderDependentAbstraction env evd flags typ (p, oplist) = -- cgit v1.2.3