diff options
| author | Maxime Dénès | 2018-09-26 15:36:26 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-26 15:36:26 +0200 |
| commit | 6a48e732577b9ab09d458c7526f599d4528fe2fc (patch) | |
| tree | 66cf1df2a49a7ee2470d13dd46b3ee917cdc00e3 /checker | |
| parent | 5ced288419aed8a622ed2c267e35d9a174facafc (diff) | |
| parent | 39a10cba3d610c6f12438084c5de7c1217c8fe94 (diff) | |
Merge PR #8534: Checking if low-level name printers are used on purpose or not
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/environ.ml | 2 | ||||
| -rw-r--r-- | checker/indtypes.ml | 6 | ||||
| -rw-r--r-- | checker/typeops.ml | 4 |
3 files changed, 8 insertions, 4 deletions
diff --git a/checker/environ.ml b/checker/environ.ml index 74cf237763..b172acb126 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -183,7 +183,7 @@ let lookup_mind kn env = let add_mind kn mib env = if Mindmap_env.mem kn env.env_globals.env_inductives then - Printf.ksprintf anomaly ("Inductive %s is already defined.") + Printf.ksprintf anomaly ("Mutual inductive block %s is already defined.") (MutInd.to_string kn); let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 8f11e01c33..1fd86bc368 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -595,8 +595,12 @@ let check_subtyping cumi paramsctxt env inds = (************************************************************************) (************************************************************************) +let print_mutind ind = + let kn = MutInd.user ind in + str (ModPath.to_string (KerName.modpath kn) ^ "." ^ Label.to_string (KerName.label kn)) + let check_inductive env kn mib = - Flags.if_verbose Feedback.msg_notice (str " checking ind: " ++ MutInd.print kn); + Flags.if_verbose Feedback.msg_notice (str " checking mutind block: " ++ print_mutind kn); (* check mind_constraints: should be consistent with env *) let env0 = match mib.mind_universes with diff --git a/checker/typeops.ml b/checker/typeops.ml index 138fe8bc95..e4c3f4ae4b 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -158,7 +158,7 @@ let judge_of_inductive_knowing_parameters env (ind,u) (paramstyp:constr array) = let specif = try lookup_mind_specif env ind with Not_found -> - failwith ("Cannot find inductive: "^MutInd.to_string (fst ind)) + failwith ("Cannot find mutual inductive block: "^MutInd.to_string (fst ind)) in type_of_inductive_knowing_parameters env (specif,u) paramstyp @@ -172,7 +172,7 @@ let judge_of_constructor env (c,u) = let specif = try lookup_mind_specif env ind with Not_found -> - failwith ("Cannot find inductive: "^MutInd.to_string (fst ind)) + failwith ("Cannot find mutual inductive block: "^MutInd.to_string (fst ind)) in type_of_constructor (c,u) specif |