diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-28 21:05:35 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-28 21:05:35 +0000 |
| commit | 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 (patch) | |
| tree | e035f490e2c748356df73342876b22cfcb3bc5a0 /checker/modops.ml | |
| parent | 5e8824960f68f529869ac299b030282cc916ba2c (diff) | |
Uniformization of the "anomaly" command.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/modops.ml')
| -rw-r--r-- | checker/modops.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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) |