From b994e3195d296e9d12c058127ced381976c3a49e Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 31 May 2016 09:09:56 +0200 Subject: Checker: avoid using obsolete names from Names --- checker/indtypes.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'checker/indtypes.ml') diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 566df673c..fd5eaeb8b 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -32,11 +32,11 @@ let string_of_mp mp = if !Flags.debug then debug_string_of_mp mp else string_of_mp mp let prkn kn = - let (mp,_,l) = repr_kn kn in + let (mp,_,l) = KerName.repr kn in str(string_of_mp mp ^ "." ^ Label.to_string l) let prcon c = - let ck = canonical_con c in - let uk = user_con c in + let ck = Constant.canonical c in + let uk = Constant.user c in if KerName.equal ck uk then prkn uk else (prkn uk ++str"(="++prkn ck++str")") (* Same as noccur_between but may perform reductions. @@ -528,7 +528,7 @@ let check_positivity env_ar mind params nrecp inds = (************************************************************************) let check_inductive env kn mib = - Flags.if_verbose ppnl (str " checking ind: " ++ pr_mind kn); pp_flush (); + Flags.if_verbose ppnl (str " checking ind: " ++ MutInd.print kn); pp_flush (); (* check mind_constraints: should be consistent with env *) let env = add_constraints (Univ.UContext.constraints mib.mind_universes) env in (* check mind_record : TODO ? check #constructor = 1 ? *) -- cgit v1.2.3