diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-13 14:23:18 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 21:55:48 +0200 |
| commit | 8c74d3e5578caeb5c62ba462528d9972c1de17f1 (patch) | |
| tree | d85d73110a1eb95b8873375cee0bd35821996657 /ltac/tacinterp.ml | |
| parent | df1e24f64f68318221d08246098837368ee1b406 (diff) | |
Passing around the precedence to the generic printer so as to solve
the remaining issue with the fix to #3709.
However, this does not solve the problem in mind which is that
"intuition idtac; idtac" is printed with extra parentheses into
"intuition (idtac; idtac)".
If one change the level of printing of TacArg of Tacexp from latom to
inherited, this breaks elsewhere, with "let x := (simpl) in idtac"
printed "let x := simpl in idtac".
Diffstat (limited to 'ltac/tacinterp.ml')
| -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 e9c30e728..e8dee7a00 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 |