diff options
Diffstat (limited to 'toplevel/class.ml')
| -rw-r--r-- | toplevel/class.ml | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index 3d6d567c..6d53ec9d 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Pp open Names @@ -32,7 +32,6 @@ type coercion_error_kind = | NotAFunction | NoSource of cl_typ option | ForbiddenSourceClass of cl_typ - | NotUniform | NoTarget | WrongTarget of cl_typ * cl_typ | NotAClass of global_reference @@ -51,9 +50,6 @@ let explain_coercion_error g = function (str ": cannot find the source class of " ++ Printer.pr_global g) | ForbiddenSourceClass cl -> pr_class cl ++ str " cannot be a source class" - | NotUniform -> - (Printer.pr_global g ++ - str" does not respect the uniform inheritance condition"); | NoTarget -> (str"Cannot find the target class") | WrongTarget (clt,cl) -> @@ -197,13 +193,13 @@ let build_id_coercion idf_opt source poly = let val_f = it_mkLambda_or_LetIn (mkLambda (Name Namegen.default_dependent_ident, - applistc vs (extended_rel_list 0 lams), + applistc vs (Context.Rel.to_extended_list 0 lams), mkRel 1)) lams in let typ_f = it_mkProd_wo_LetIn - (mkProd (Anonymous, applistc vs (extended_rel_list 0 lams), lift 1 t)) + (mkProd (Anonymous, applistc vs (Context.Rel.to_extended_list 0 lams), lift 1 t)) lams in (* juste pour verification *) @@ -247,6 +243,12 @@ booleen "coercion identite'?" lorque source est None alors target est None aussi. *) +let warn_uniform_inheritance = + CWarnings.create ~name:"uniform-inheritance" ~category:"typechecker" + (fun g -> + Printer.pr_global g ++ + strbrk" does not respect the uniform inheritance condition") + let add_new_coercion_core coef stre poly source target isid = check_source source; let t = Global.type_of_global_unsafe coef in @@ -262,7 +264,7 @@ let add_new_coercion_core coef stre poly source target isid = in check_source (Some cls); if not (uniform_cond (llp-ind) lvs) then - msg_warning (explain_coercion_error coef NotUniform); + warn_uniform_inheritance coef; let clt = try get_target tg ind @@ -310,7 +312,7 @@ let add_coercion_hook poly local ref = in let () = try_add_new_coercion ref stre poly in let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in - Flags.if_verbose msg_info msg + Flags.if_verbose Feedback.msg_info msg let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly) |