From 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Mon, 28 Jan 2013 21:05:35 +0000 Subject: Uniformization of the "anomaly" command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/modops.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'checker/modops.ml') diff --git a/checker/modops.ml b/checker/modops.ml index f9c52c2e9..6b7a9c7a1 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -90,7 +90,7 @@ and add_module mb env = | SEBstruct (sign) -> add_signature mp sign mb.mod_delta env | SEBfunctor _ -> env - | _ -> anomaly "Modops:the evaluation of the structure failed " + | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ") let strengthen_const mp_from l cb resolver = @@ -118,7 +118,7 @@ let rec strengthen_mod mp_from mp_to mb = (add_delta_resolver mb.mod_delta resolve_out)*); mod_retroknowledge = mb.mod_retroknowledge} | SEBfunctor _ -> mb - | _ -> anomaly "Modops:the evaluation of the structure failed " + | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ") and strengthen_sig mp_from sign mp_to resolver = match sign with @@ -152,7 +152,7 @@ let strengthen mtb mp = typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta (add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)} | SEBfunctor _ -> mtb - | _ -> anomaly "Modops:the evaluation of the structure failed " + | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ") let subst_and_strengthen mb mp = strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb) -- cgit v1.2.3