diff options
Diffstat (limited to 'toplevel/himsg.ml')
| -rw-r--r-- | toplevel/himsg.ml | 351 |
1 files changed, 272 insertions, 79 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 62d19bea..f550df16 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: himsg.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Flags @@ -28,12 +26,13 @@ open Reduction open Cases open Logic open Printer -open Rawterm +open Glob_term open Evd +open Libnames +open Declarations let pr_lconstr c = quote (pr_lconstr c) let pr_lconstr_env e c = quote (pr_lconstr_env e c) -let pr_lconstr_env_at_top e c = quote (pr_lconstr_env_at_top e c) let pr_ljudge_env e c = let v,t = pr_ljudge_env e c in (quote v,quote t) let pr_db env i = @@ -52,7 +51,8 @@ let explain_unbound_var env v = let var = pr_id v in str "No such section variable or assumption: " ++ var ++ str "." -let explain_not_type env j = +let explain_not_type env sigma j = + let j = j_nf_evar sigma j in let pe = pr_ne_context_of (str "In environment") env in let pc,pt = pr_ljudge_env env j in pe ++ str "The term" ++ brk(1,1) ++ pc ++ spc () ++ @@ -111,7 +111,8 @@ let explain_elim_arity env ind sorts c pj okinds = str "in the inductive type" ++ spc () ++ quote pi ++ str ":") ++ fnl () ++ msg -let explain_case_not_inductive env cj = +let explain_case_not_inductive env sigma cj = + let cj = j_nf_evar sigma cj in let env = make_all_name_different env in let pc = pr_lconstr_env env cj.uj_val in let pct = pr_lconstr_env env cj.uj_type in @@ -123,7 +124,8 @@ let explain_case_not_inductive env cj = str "has type" ++ brk(1,1) ++ pct ++ spc () ++ str "which is not a (co-)inductive type." -let explain_number_branches env cj expn = +let explain_number_branches env sigma cj expn = + let cj = j_nf_evar sigma cj in let env = make_all_name_different env in let pc = pr_lconstr_env env cj.uj_val in let pct = pr_lconstr_env env cj.uj_type in @@ -131,14 +133,17 @@ let explain_number_branches env cj expn = str "of type" ++ brk(1,1) ++ pct ++ spc () ++ str "expects " ++ int expn ++ str " branches." -let explain_ill_formed_branch env c i actty expty = +let explain_ill_formed_branch env sigma c ci actty expty = + let simp t = Reduction.nf_betaiota (nf_evar sigma t) in + let c = nf_evar sigma c in let env = make_all_name_different env in let pc = pr_lconstr_env env c in - let pa = pr_lconstr_env env actty in - let pe = pr_lconstr_env env expty in - str "In pattern-matching on term" ++ brk(1,1) ++ pc ++ - spc () ++ str "the " ++ nth (i+1) ++ str " branch has type" ++ - brk(1,1) ++ pa ++ spc () ++ + let pa = pr_lconstr_env env (simp actty) in + let pe = pr_lconstr_env env (simp expty) in + strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++ + spc () ++ strbrk "the branch for constructor" ++ spc () ++ + quote (pr_constructor env ci) ++ + spc () ++ str "has type" ++ brk(1,1) ++ pa ++ spc () ++ str "which should be" ++ brk(1,1) ++ pe ++ str "." let explain_generalization env (name,var) j = @@ -150,7 +155,9 @@ let explain_generalization env (name,var) j = str "it has type" ++ spc () ++ pt ++ spc () ++ str "which should be Set, Prop or Type." -let explain_actual_type env j pt = +let explain_actual_type env sigma j pt = + let j = j_nf_betaiotaevar sigma j in + let pt = Reductionops.nf_betaiota sigma pt in let pe = pr_ne_context_of (str "In environment") env in let (pc,pct) = pr_ljudge_env env j in let pt = pr_lconstr_env env pt in @@ -159,7 +166,11 @@ let explain_actual_type env j pt = str "has type" ++ brk(1,1) ++ pct ++ brk(1,1) ++ str "while it is expected to have type" ++ brk(1,1) ++ pt ++ str "." -let explain_cant_apply_bad_type env (n,exptyp,actualtyp) rator randl = +let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = + let randl = jv_nf_betaiotaevar sigma randl in + let exptyp = nf_evar sigma exptyp in + let actualtyp = Reductionops.nf_betaiota sigma actualtyp in + let rator = j_nf_evar sigma rator in let env = make_all_name_different env in let nargs = Array.length randl in (* let pe = pr_ne_context_of (str "in environment") env in*) @@ -181,7 +192,9 @@ let explain_cant_apply_bad_type env (n,exptyp,actualtyp) rator randl = str "which should be coercible to" ++ brk(1,1) ++ pr_lconstr_env env exptyp ++ str "." -let explain_cant_apply_not_functional env rator randl = +let explain_cant_apply_not_functional env sigma rator randl = + let randl = jv_nf_evar sigma randl in + let rator = j_nf_evar sigma rator in let env = make_all_name_different env in let nargs = Array.length randl in (* let pe = pr_ne_context_of (str "in environment") env in*) @@ -200,14 +213,16 @@ let explain_cant_apply_not_functional env rator randl = str "cannot be applied to the " ++ str (plural nargs "term") ++ fnl () ++ str " " ++ v 0 appl -let explain_unexpected_type env actual_type expected_type = +let explain_unexpected_type env sigma actual_type expected_type = + let actual_type = nf_evar sigma actual_type in + let expected_type = nf_evar sigma expected_type in let pract = pr_lconstr_env env actual_type in let prexp = pr_lconstr_env env expected_type in - str "This type is" ++ spc () ++ pract ++ spc () ++ - str "but is expected to be" ++ - spc () ++ prexp ++ str "." + str "Found type" ++ spc () ++ pract ++ spc () ++ + str "where" ++ spc () ++ prexp ++ str " was expected." -let explain_not_product env c = +let explain_not_product env sigma c = + let c = nf_evar sigma c in let pr = pr_lconstr_env env c in str "The type of this term is a product" ++ spc () ++ str "while it is expected to be" ++ @@ -229,7 +244,8 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = | RecursionNotOnInductiveType c -> str "Recursive definition on" ++ spc () ++ pr_lconstr_env env c ++ spc () ++ str "which should be an inductive type" - | RecursionOnIllegalTerm(j,arg,le,lt) -> + | RecursionOnIllegalTerm(j,(arg_env, arg),le,lt) -> + let arg_env = make_all_name_different arg_env in let called = match names.(j) with Name id -> pr_id id @@ -247,7 +263,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = prlist_with_sep pr_spc pr_db lt in str "Recursive call to " ++ called ++ spc () ++ strbrk "has principal argument equal to" ++ spc () ++ - pr_lconstr_env env arg ++ strbrk " instead of " ++ vars + pr_lconstr_env arg_env arg ++ strbrk " instead of " ++ vars | NotEnoughArgumentsForFixCall j -> let called = @@ -274,12 +290,12 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = str "Recursive call forbidden in the type of a recursive definition" ++ spc () ++ pr_lconstr_env env c | RecCallInCaseFun c -> - str "Recursive call in a branch of" ++ spc () ++ pr_lconstr_env env c + str "Invalid recursive call in a branch of" ++ spc () ++ pr_lconstr_env env c | RecCallInCaseArg c -> - str "Recursive call in the argument of cases in" ++ spc () ++ + str "Invalid recursive call in the argument of \"match\" in" ++ spc () ++ pr_lconstr_env env c | RecCallInCasePred c -> - str "Recursive call in the type of cases in" ++ spc () ++ + str "Invalid recursive call in the \"return\" clause of \"match\" in" ++ spc () ++ pr_lconstr_env env c | NotGuardedForm c -> str "Sub-expression " ++ pr_lconstr_env env c ++ @@ -293,9 +309,11 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = let fixenv = make_all_name_different fixenv in let pvd = pr_lconstr_env fixenv vdefj.(i).uj_val in str"Recursive definition is:" ++ spc () ++ pvd ++ str "." - with _ -> mt ()) + with e when Errors.noncritical e -> mt ()) -let explain_ill_typed_rec_body env i names vdefj vargs = +let explain_ill_typed_rec_body env sigma i names vdefj vargs = + let vdefj = jv_nf_evar sigma vdefj in + let vargs = Array.map (nf_evar sigma) vargs in let env = make_all_name_different env in let pvd,pvdt = pr_ljudge_env env (vdefj.(i)) in let pv = pr_lconstr_env env vargs.(i) in @@ -305,12 +323,14 @@ let explain_ill_typed_rec_body env i names vdefj vargs = str "has type" ++ spc () ++ pvdt ++ spc () ++ str "while it should be" ++ spc () ++ pv ++ str "." -let explain_cant_find_case_type env c = +let explain_cant_find_case_type env sigma c = + let c = nf_evar sigma c in let env = make_all_name_different env in let pe = pr_lconstr_env env c in str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe ++ str "." -let explain_occur_check env ev rhs = +let explain_occur_check env sigma ev rhs = + let rhs = nf_evar sigma rhs in let env = make_all_name_different env in let id = Evd.string_of_existential ev in let pt = pr_lconstr_env env rhs in @@ -354,7 +374,8 @@ let explain_hole_kind env evi = function | MatchingVar _ -> assert false -let explain_not_clean env ev t k = +let explain_not_clean env sigma ev t k = + let t = nf_evar sigma t in let env = make_all_name_different env in let id = Evd.string_of_existential ev in let var = pr_lconstr_env env t in @@ -369,15 +390,12 @@ let explain_unsolvability = function strbrk " (several distinct possible instances found)" let explain_typeclass_resolution env evi k = - match k with - | GoalEvar | InternalHole | ImplicitArg _ -> - (match Typeclasses.class_of_constr evi.evar_concl with - | Some c -> - let env = Evd.evar_env evi in - fnl () ++ str "Could not find an instance for " ++ - pr_lconstr_env env evi.evar_concl ++ - pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env - | None -> mt()) + match Typeclasses.class_of_constr evi.evar_concl with + | Some c -> + let env = Evd.evar_env evi in + fnl () ++ str "Could not find an instance for " ++ + pr_lconstr_env env evi.evar_concl ++ + pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env | _ -> mt() let explain_unsolvable_implicit env evi k explain = @@ -401,13 +419,15 @@ let explain_wrong_case_info env ind ci = str "was given to a pattern-matching expression on the inductive type" ++ spc () ++ pc ++ str "." -let explain_cannot_unify env m n = +let explain_cannot_unify env sigma m n = + let m = nf_evar sigma m in + let n = nf_evar sigma n in let pm = pr_lconstr_env env m in let pn = pr_lconstr_env env n in str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ str "with" ++ brk(1,1) ++ pn ++ str "." -let explain_cannot_unify_local env m n subn = +let explain_cannot_unify_local env sigma m n subn = let pm = pr_lconstr_env env m in let pn = pr_lconstr_env env n in let psubn = pr_lconstr_env env subn in @@ -449,7 +469,7 @@ let explain_non_linear_unification env m t = strbrk " which would require to abstract twice on " ++ pr_lconstr_env env t ++ str "." -let explain_type_error env err = +let explain_type_error env sigma err = let env = make_all_name_different env in match err with | UnboundRel n -> @@ -457,7 +477,7 @@ let explain_type_error env err = | UnboundVar v -> explain_unbound_var env v | NotAType j -> - explain_not_type env j + explain_not_type env sigma j | BadAssumption c -> explain_bad_assumption env c | ReferenceVariables id -> @@ -465,38 +485,39 @@ let explain_type_error env err = | ElimArity (ind, aritylst, c, pj, okinds) -> explain_elim_arity env ind aritylst c pj okinds | CaseNotInductive cj -> - explain_case_not_inductive env cj + explain_case_not_inductive env sigma cj | NumberBranches (cj, n) -> - explain_number_branches env cj n + explain_number_branches env sigma cj n | IllFormedBranch (c, i, actty, expty) -> - explain_ill_formed_branch env c i actty expty + explain_ill_formed_branch env sigma c i actty expty | Generalization (nvar, c) -> explain_generalization env nvar c | ActualType (j, pt) -> - explain_actual_type env j pt + explain_actual_type env sigma j pt | CantApplyBadType (t, rator, randl) -> - explain_cant_apply_bad_type env t rator randl + explain_cant_apply_bad_type env sigma t rator randl | CantApplyNonFunctional (rator, randl) -> - explain_cant_apply_not_functional env rator randl + explain_cant_apply_not_functional env sigma rator randl | IllFormedRecBody (err, lna, i, fixenv, vdefj) -> explain_ill_formed_rec_body env err lna i fixenv vdefj | IllTypedRecBody (i, lna, vdefj, vargs) -> - explain_ill_typed_rec_body env i lna vdefj vargs + explain_ill_typed_rec_body env sigma i lna vdefj vargs | WrongCaseInfo (ind,ci) -> explain_wrong_case_info env ind ci -let explain_pretype_error env err = +let explain_pretype_error env sigma err = + let env = env_nf_betaiotaevar sigma env in let env = make_all_name_different env in match err with - | CantFindCaseType c -> explain_cant_find_case_type env c - | OccurCheck (n,c) -> explain_occur_check env n c - | NotClean (n,c,k) -> explain_not_clean env n c k + | CantFindCaseType c -> explain_cant_find_case_type env sigma c + | OccurCheck (n,c) -> explain_occur_check env sigma n c + | NotClean (n,c,k) -> explain_not_clean env sigma n c k | UnsolvableImplicit (evi,k,exp) -> explain_unsolvable_implicit env evi k exp | VarNotFound id -> explain_var_not_found env id - | UnexpectedType (actual,expect) -> explain_unexpected_type env actual expect - | NotProduct c -> explain_not_product env c - | CannotUnify (m,n) -> explain_cannot_unify env m n - | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env m n sn + | UnexpectedType (actual,expect) -> explain_unexpected_type env sigma actual expect + | NotProduct c -> explain_not_product env sigma c + | CannotUnify (m,n) -> explain_cannot_unify env sigma m n + | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env sigma m n sn | CannotGeneralize ty -> explain_refiner_cannot_generalize env ty | NoOccurrenceFound (c, id) -> explain_no_occurrence_found env c id | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n @@ -504,6 +525,158 @@ let explain_pretype_error env err = explain_cannot_find_well_typed_abstraction env p l | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n | NonLinearUnification (m,c) -> explain_non_linear_unification env m c + | TypingError t -> explain_type_error env sigma t + +(* Module errors *) + +open Modops + +let explain_not_match_error = function + | InductiveFieldExpected _ -> + strbrk "an inductive definition is expected" + | DefinitionFieldExpected -> + strbrk "a definition is expected" + | ModuleFieldExpected -> + strbrk "a module is expected" + | ModuleTypeFieldExpected -> + strbrk "a module type is expected" + | NotConvertibleInductiveField id | NotConvertibleConstructorField id -> + str "types given to " ++ str (string_of_id id) ++ str " differ" + | NotConvertibleBodyField -> + str "the body of definitions differs" + | NotConvertibleTypeField (env, typ1, typ2) -> + str "expected type" ++ spc () ++ + quote (Printer.safe_pr_lconstr_env env typ2) ++ spc () ++ + str "but found type" ++ spc () ++ + quote (Printer.safe_pr_lconstr_env env typ1) + | NotSameConstructorNamesField -> + str "constructor names differ" + | NotSameInductiveNameInBlockField -> + str "inductive types names differ" + | FiniteInductiveFieldExpected isfinite -> + str "type is expected to be " ++ + str (if isfinite then "coinductive" else "inductive") + | InductiveNumbersFieldExpected n -> + str "number of inductive types differs" + | InductiveParamsNumberField n -> + str "inductive type has not the right number of parameters" + | RecordFieldExpected isrecord -> + str "type is expected " ++ str (if isrecord then "" else "not ") ++ + str "to be a record" + | RecordProjectionsExpected nal -> + (if List.length nal >= 2 then str "expected projection names are " + else str "expected projection name is ") ++ + pr_enum (function Name id -> str (string_of_id id) | _ -> str "_") nal + | NotEqualInductiveAliases -> + str "Aliases to inductive types do not match" + | NoTypeConstraintExpected -> + strbrk "a definition whose type is constrained can only be subtype of a definition whose type is itself constrained" + +let explain_signature_mismatch l spec why = + str "Signature components for label " ++ str (string_of_label l) ++ + str " do not match:" ++ spc () ++ explain_not_match_error why ++ str "." + +let explain_label_already_declared l = + str ("The label "^string_of_label l^" is already declared.") + +let explain_application_to_not_path _ = + str "Application of modules is restricted to paths." + +let explain_not_a_functor mtb = + str "Application of not a functor." + +let explain_incompatible_module_types mexpr1 mexpr2 = + str "Incompatible module types." + +let explain_not_equal_module_paths mp1 mp2 = + str "Non equal modules." + +let explain_no_such_label l = + str "No such label " ++ str (string_of_label l) ++ str "." + +let explain_incompatible_labels l l' = + str "Opening and closing labels are not the same: " ++ + str (string_of_label l) ++ str " <> " ++ str (string_of_label l') ++ str "!" + +let explain_signature_expected mtb = + str "Signature expected." + +let explain_no_module_to_end () = + str "No open module to end." + +let explain_no_module_type_to_end () = + str "No open module type to end." + +let explain_not_a_module s = + quote (str s) ++ str " is not a module." + +let explain_not_a_module_type s = + quote (str s) ++ str " is not a module type." + +let explain_not_a_constant l = + quote (pr_label l) ++ str " is not a constant." + +let explain_incorrect_label_constraint l = + str "Incorrect constraint for label " ++ + quote (pr_label l) ++ str "." + +let explain_generative_module_expected l = + str "The module " ++ str (string_of_label l) ++ + strbrk " is not generative. Only components of generative modules can be changed using the \"with\" construct." + +let explain_non_empty_local_context = function + | None -> str "The local context is not empty." + | Some l -> + str "The local context of the component " ++ + str (string_of_label l) ++ str " is not empty." + +let explain_label_missing l s = + str "The field " ++ str (string_of_label l) ++ str " is missing in " + ++ str s ++ str "." + +let explain_module_error = function + | SignatureMismatch (l,spec,err) -> explain_signature_mismatch l spec err + | LabelAlreadyDeclared l -> explain_label_already_declared l + | ApplicationToNotPath mexpr -> explain_application_to_not_path mexpr + | NotAFunctor mtb -> explain_not_a_functor mtb + | IncompatibleModuleTypes (m1,m2) -> explain_incompatible_module_types m1 m2 + | NotEqualModulePaths (mp1,mp2) -> explain_not_equal_module_paths mp1 mp2 + | NoSuchLabel l -> explain_no_such_label l + | IncompatibleLabels (l1,l2) -> explain_incompatible_labels l1 l2 + | SignatureExpected mtb -> explain_signature_expected mtb + | NoModuleToEnd -> explain_no_module_to_end () + | NoModuleTypeToEnd -> explain_no_module_type_to_end () + | NotAModule s -> explain_not_a_module s + | NotAModuleType s -> explain_not_a_module_type s + | NotAConstant l -> explain_not_a_constant l + | IncorrectWithConstraint l -> explain_incorrect_label_constraint l + | GenerativeModuleExpected l -> explain_generative_module_expected l + | NonEmptyLocalContect lopt -> explain_non_empty_local_context lopt + | LabelMissing (l,s) -> explain_label_missing l s + +(* Module internalization errors *) + +(* +let explain_declaration_not_path _ = + str "Declaration is not a path." + +*) + +let explain_not_module_nor_modtype s = + quote (str s) ++ str " is not a module or module type." + +let explain_incorrect_with_in_module () = + str "The syntax \"with\" is not allowed for modules." + +let explain_incorrect_module_application () = + str "Illegal application to a module type." + +open Modintern + +let explain_module_internalization_error = function + | NotAModuleNorModtype s -> explain_not_module_nor_modtype s + | IncorrectWithInModule -> explain_incorrect_with_in_module () + | IncorrectModuleApplication -> explain_incorrect_module_application () (* Typeclass errors *) @@ -524,8 +697,11 @@ let explain_no_instance env (_,id) l = str "applied to arguments" ++ spc () ++ prlist_with_sep pr_spc (pr_lconstr_env env) l +let is_goal_evar evi = match evi.evar_source with (_, GoalEvar) -> true | _ -> false + let pr_constraints printenv env evm = let l = Evd.to_list evm in + assert(l <> []); let (ev, evi) = List.hd l in if List.for_all (fun (ev', evi') -> eq_named_context_val evi.evar_hyps evi'.evar_hyps) l @@ -534,23 +710,30 @@ let pr_constraints printenv env evm = (reset_with_named_context evi.evar_hyps env) in (if printenv then pe ++ fnl () else mt ()) ++ prlist_with_sep (fun () -> fnl ()) - (fun (ev, evi) -> str(string_of_existential ev)++ str " == " ++ pr_constr evi.evar_concl) l + (fun (ev, evi) -> str(string_of_existential ev) ++ + str " : " ++ pr_lconstr evi.evar_concl) l ++ fnl() ++ + pr_evar_map_constraints evm else - pr_evar_map evm + pr_evar_map None evm let explain_unsatisfiable_constraints env evd constr = - let evm = Evarutil.nf_evars evd in - let undef = Evd.undefined_evars evm in + let evm = Evd.undefined_evars (Evarutil.nf_evar_map_undefined evd) in + (* Remove goal evars *) + let undef = fold_undefined + (fun ev evi evm' -> + if is_goal_evar evi then Evd.remove evm' ev else evm') evm evm + in match constr with | None -> str"Unable to satisfy the following constraints:" ++ fnl() ++ pr_constraints true env undef | Some (ev, k) -> - explain_unsolvable_implicit env (Evd.find evm ev) k None ++ fnl () ++ - if List.length (Evd.to_list undef) > 1 then - str"With the following constraints:" ++ fnl() ++ - pr_constraints false env (Evd.remove undef ev) - else mt () + explain_typeclass_resolution env (Evd.find evm ev) k ++ fnl () ++ + (let remaining = Evd.remove undef ev in + if Evd.has_undefined remaining then + str"With the following constraints:" ++ fnl() ++ + pr_constraints false env remaining + else mt ()) let explain_mismatched_contexts env c i j = str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++ @@ -644,8 +827,12 @@ let error_ill_formed_constructor env id c v nparams nargs = else mt()) ++ str "." +let pr_ltype_using_barendregt_convention_env env c = + (* Use goal_concl_style as an approximation of Barendregt's convention (?) *) + quote (pr_goal_concl_style_env env c) + let error_bad_ind_parameters env c n v1 v2 = - let pc = pr_lconstr_env_at_top env c in + let pc = pr_ltype_using_barendregt_convention_env env c in let pv1 = pr_lconstr_env env v1 in let pv2 = pr_lconstr_env env v2 in str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++ @@ -684,7 +871,7 @@ let error_not_allowed_case_analysis isrec kind i = let error_not_mutual_in_scheme ind ind' = if ind = ind' then str "The inductive type " ++ pr_inductive (Global.env()) ind ++ - str "occurs twice." + str " occurs twice." else str "The inductive types " ++ pr_inductive (Global.env()) ind ++ spc () ++ str "and" ++ spc () ++ pr_inductive (Global.env()) ind' ++ spc () ++ @@ -803,13 +990,19 @@ let explain_pattern_matching_error env = function let explain_reduction_tactic_error = function | Tacred.InvalidAbstraction (env,c,(env',e)) -> - str "The abstracted term" ++ spc () ++ pr_lconstr_env_at_top env c ++ + str "The abstracted term" ++ spc () ++ + quote (pr_goal_concl_style_env env c) ++ spc () ++ str "is not well typed." ++ fnl () ++ - explain_type_error env' e + explain_type_error env' Evd.empty e let explain_ltac_call_trace (nrep,last,trace,loc) = let calls = (nrep,last) :: List.rev (List.map(fun(n,_,ck)->(n,ck))trace) in + let tacexpr_differ te te' = + (* NB: The following comparison may raise an exception + since a tacexpr may embed a functional part via a TacExtend *) + try te <> te' with Invalid_argument _ -> false + in let pr_call (n,ck) = (match ck with | Proof_type.LtacNotationCall s -> quote (str s) @@ -821,17 +1014,17 @@ let explain_ltac_call_trace (nrep,last,trace,loc) = (Pptactic.pr_glob_tactic (Global.env()) (Tacexpr.TacAtom (dummy_loc,te))) ++ (match !otac with - | Some te' when (Obj.magic te' <> te) -> - strbrk " (expanded to " ++ quote - (Pptactic.pr_tactic (Global.env()) - (Tacexpr.TacAtom (dummy_loc,te'))) - ++ str ")" + | Some te' when tacexpr_differ (Obj.magic te') te -> + strbrk " (expanded to " ++ quote + (Pptactic.pr_tactic (Global.env()) + (Tacexpr.TacAtom (dummy_loc,te'))) + ++ str ")" | _ -> mt ()) | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) -> let filter = function (id,None) -> None | (id,Some id') -> Some(id,([],mkVar id')) in let unboundvars = list_map_filter filter unboundvars in - quote (pr_rawconstr_env (Global.env()) c) ++ + quote (pr_glob_constr_env (Global.env()) c) ++ (if unboundvars <> [] or vars <> [] then strbrk " (with " ++ prlist_with_sep pr_comma |