diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cbv.ml | 8 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 2 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 14 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 9 |
4 files changed, 17 insertions, 16 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index fc24e9b3a9..265909980b 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -187,7 +187,7 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> debug_cbv:=a); } -let pr_key = function +let debug_pr_key = function | ConstKey (sp,_) -> Names.Constant.print sp | VarKey id -> Names.Id.print id | RelKey n -> Pp.(str "REL_" ++ int n) @@ -320,14 +320,14 @@ and norm_head_ref k info env stack normt = if red_set_ref (info_flags info.infos) normt then match ref_value_cache info.infos info.tab normt with | Some body -> - if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ pr_key normt); + if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt); strip_appl (shift_value k body) stack | None -> - if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt); + if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); (VAL(0,make_constr_ref k normt),stack) else begin - if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt); + if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); (VAL(0,make_constr_ref k normt),stack) end diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index ec0ff73062..b040e63cd2 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -358,7 +358,7 @@ let make_case_or_project env sigma indf ci pred c branches = not (has_dependent_elim mib) then user_err ~hdr:"make_case_or_project" Pp.(str"Dependent case analysis not allowed" ++ - str" on inductive type " ++ Names.MutInd.print (fst ind)) + str" on inductive type " ++ print_constr_env env sigma (mkInd ind)) in let branch = branches.(0) in let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index bd41e61b34..77ad96d2cf 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -334,19 +334,19 @@ let error_not_structure ref description = user_err ~hdr:"object_declare" (str"Could not declare a canonical structure " ++ (Id.print (basename_of_global ref) ++ str"." ++ spc() ++ - str(description))) + description)) let check_and_decompose_canonical_structure ref = let sp = match ref with ConstRef sp -> sp - | _ -> error_not_structure ref "Expected an instance of a record or structure." + | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in let env = Global.env () in let u = Univ.make_abstract_instance (Environ.constant_context env sp) in let vc = match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc - | None -> error_not_structure ref "Could not find its value in the global environment." in + | None -> error_not_structure ref (str "Could not find its value in the global environment.") in let env = Global.env () in let evd = Evd.from_env env in let body = snd (splay_lam (Global.env()) evd (EConstr.of_constr vc)) in @@ -354,18 +354,18 @@ let check_and_decompose_canonical_structure ref = let f,args = match kind body with | App (f,args) -> f,args | _ -> - error_not_structure ref "Expected a record or structure constructor applied to arguments." in + error_not_structure ref (str "Expected a record or structure constructor applied to arguments.") in let indsp = match kind f with | Construct ((indsp,1),u) -> indsp - | _ -> error_not_structure ref "Expected an instance of a record or structure." in + | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in let s = try lookup_structure indsp with Not_found -> error_not_structure ref - ("Could not find the record or structure " ^ (MutInd.to_string (fst indsp))) in + (str "Could not find the record or structure " ++ Termops.print_constr (EConstr.mkInd indsp)) in let ntrue_projs = List.count snd s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then - error_not_structure ref "Got too few arguments to the record or structure constructor."; + error_not_structure ref (str "Got too few arguments to the record or structure constructor."); (sp,indsp) let declare_canonical_structure ref = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index f4c8a6cd66..a0d20b7ce4 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -341,6 +341,7 @@ struct | Cst of cst_member * int * int list * 'a t * Cst_stack.t and 'a t = 'a member list + (* Debugging printer *) let rec pr_member pr_c member = let open Pp in let pr_c x = hov 1 (pr_c x) in @@ -351,7 +352,7 @@ struct prvect_with_sep (pr_bar) pr_c br ++ str ")" | Proj (p,cst) -> - str "ZProj(" ++ Constant.print (Projection.constant p) ++ str ")" + str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")" | Fix (f,args,cst) -> str "ZFix(" ++ Termops.pr_fix pr_c f ++ pr_comma () ++ pr pr_c args ++ str ")" @@ -368,11 +369,11 @@ struct let open Pp in match c with | Cst_const (c, u) -> - if Univ.Instance.is_empty u then Constant.print c - else str"(" ++ Constant.print c ++ str ", " ++ + if Univ.Instance.is_empty u then Constant.debug_print c + else str"(" ++ Constant.debug_print c ++ str ", " ++ Univ.Instance.pr Univ.Level.pr u ++ str")" | Cst_proj p -> - str".(" ++ Constant.print (Projection.constant p) ++ str")" + str".(" ++ Constant.debug_print (Projection.constant p) ++ str")" let empty = [] let is_empty = CList.is_empty |