diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-21 21:11:17 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-21 21:11:17 +0000 |
| commit | 5cff8a26e6444a4523eb8f471a1203a33c611b5b (patch) | |
| tree | a6cdc580245c6390deb7f7b26f86bf60fe9e9a15 /kernel/subtyping.ml | |
| parent | 4da7ddb8c3c2f1dafd5d9187741659a9332b75c2 (diff) | |
Robust display of NotConvertibleTypeField errors (fix #3008, #2995)
Since the nametab isn't aware of everything needed to print mismatched
types (cf the bug test-cases), we create a robust term printer that
known how to print a fully-qualified name when [shortest_qualid_of_global]
has failed. These Printer.safe_pr_constr and alii are meant to never fail
(at worse they display "??", for instance when the env isn't rich enough).
Moreover, the environnement may have changed between the raise
of NotConvertibleTypeField and its display, so we store the original
env in the exception.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16342 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index e5b81c72f..99c1b8483 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -219,7 +219,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let check_conv cst f = check_conv_error error cst f in let check_type cst env t1 t2 = - let err = NotConvertibleTypeField (t1, t2) in + let err = NotConvertibleTypeField (env, t1, t2) in (* If the type of a constant is generated, it may mention non-variable algebraic universes that the general conversion @@ -303,7 +303,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = if Declareops.constant_has_body cb2 then error DefinitionFieldExpected; let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in let typ2 = Typeops.type_of_constant_type env cb2.const_type in - let error = NotConvertibleTypeField (arity1, typ2) in + let error = NotConvertibleTypeField (env, arity1, typ2) in check_conv error cst conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> ignore (Errors.error ( @@ -315,7 +315,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = if Declareops.constant_has_body cb2 then error DefinitionFieldExpected; let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in let ty2 = Typeops.type_of_constant_type env cb2.const_type in - let error = NotConvertibleTypeField (ty1, ty2) in + let error = NotConvertibleTypeField (env, ty1, ty2) in check_conv error cst conv env ty1 ty2 let rec check_modules cst env msb1 msb2 subst1 subst2 = |