diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index a0d20b7ce4..5dbe95a471 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -132,8 +132,7 @@ module ReductionBehaviour = struct { b with b_nargs = nargs'; b_recargs = recargs' } else b in - let c = Lib.discharge_con c in - Some (ReqGlobal (ConstRef c, req), (ConstRef c, b)) + Some (ReqGlobal (gr, req), (ConstRef c, b)) | _ -> None let rebuild = function @@ -254,9 +253,9 @@ module Cst_stack = struct (applist (cst, List.rev params)) t) cst_l c - let pr l = + let pr env sigma l = let open Pp in - let p_c c = Termops.print_constr c in + let p_c c = Termops.Internal.print_constr_env env sigma c in prlist_with_sep pr_semicolon (fun (c,params,args) -> hov 1 (str"(" ++ p_c c ++ str ")" ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++ @@ -615,9 +614,9 @@ type contextual_state_reduction_function = type state_reduction_function = contextual_state_reduction_function type local_state_reduction_function = evar_map -> state -> state -let pr_state (tm,sk) = +let pr_state env sigma (tm,sk) = let open Pp in - let pr c = Termops.print_constr c in + let pr c = Termops.Internal.print_constr_env env sigma c in h 0 (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk) (*************************************) @@ -713,8 +712,8 @@ let magicaly_constant_of_fixbody env sigma reference bd = function | Name.Name id -> let open UnivProblem in try - let (cst_mod,cst_sect,_) = Constant.repr3 reference in - let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in + let (cst_mod,_) = Constant.repr2 reference in + let cst = Constant.make2 cst_mod (Label.of_id id) in let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in match constant_opt_value_in env (cst,u) with | None -> bd @@ -855,10 +854,10 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let rec whrec cst_l (x, stack) = let () = if !debug_RAKAM then let open Pp in - let pr c = Termops.print_constr c in + let pr c = Termops.Internal.print_constr_env env sigma c in Feedback.msg_notice (h 0 (str "<<" ++ pr x ++ - str "|" ++ cut () ++ Cst_stack.pr cst_l ++ + str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++ str "|" ++ cut () ++ Stack.pr pr stack ++ str ">>")) in |