diff options
| author | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
| commit | 3d1ef11e4a70e61bb8b4c6e2c1414a19ceb42886 (patch) | |
| tree | e37edba3d78858741fb7c5c6c22a511215705f05 /ltac | |
| parent | 18512ba12400e30858ae19e5ef69b9590b96de06 (diff) | |
Revert "Passing around the precedence to the generic printer so as to solve"
This reverts commit 8c74d3e5578caeb5c62ba462528d9972c1de17f1.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/tacinterp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index e8dee7a001..e9c30e728f 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1281,7 +1281,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with in let tac = Ftactic.with_env interp_vars >>= fun (env, lr) -> - let name () = Pptactic.pr_alias (fun _ v -> print_top_val env v) 0 s lr in + let name () = Pptactic.pr_alias (fun v -> print_top_val env v) 0 s lr in Proofview.Trace.name_tactic name (tac lr) (* spiwack: this use of name_tactic is not robust to a change of implementation of [Ftactic]. In such a situation, @@ -1303,7 +1303,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let tac = Tacenv.interp_ml_tactic opn in let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in let tac args = - let name () = Pptactic.pr_extend (fun _ v -> print_top_val () v) 0 opn args in + let name () = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in Proofview.Trace.name_tactic name (catch_error_tac trace (tac args ist)) in Ftactic.run args tac |