diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-24 18:18:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:38 +0100 |
| commit | 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 (patch) | |
| tree | ae729d05933776d718905029f0a87722716ec57f /pretyping/reductionops.ml | |
| parent | 531590c223af42c07a93142ab0cea470a98964e6 (diff) | |
Ltac now uses evar-based constrs.
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 90c5b241b..bc5c629f4 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -210,7 +210,7 @@ module Cst_stack = struct let pr l = let open Pp in - let p_c c = Termops.print_constr (EConstr.Unsafe.to_constr c) in + let p_c c = Termops.print_constr 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:" ++ @@ -606,7 +606,7 @@ type local_state_reduction_function = evar_map -> state -> state let pr_state (tm,sk) = let open Pp in - let pr c = Termops.print_constr (EConstr.Unsafe.to_constr c) in + let pr c = Termops.print_constr c in h 0 (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk) let local_assum (na, t) = @@ -835,7 +835,7 @@ 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 (EConstr.Unsafe.to_constr c) in + let pr c = Termops.print_constr c in Feedback.msg_notice (h 0 (str "<<" ++ pr x ++ str "|" ++ cut () ++ Cst_stack.pr cst_l ++ |