diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacinterp.ml | 7 | ||||
| -rw-r--r-- | proofs/tacinterp.mli | 5 |
2 files changed, 11 insertions, 1 deletions
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 74fc4fb292..c98840d731 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -1149,6 +1149,13 @@ let interp_tacarg sign ast = unvarg (val_interp sign ast) (* Initial call for interpretation *) let interp = fun ast -> tac_interp [] [] !debug ast +(* Hides interpretation for pretty-print *) +let hide_interp = + let htac = hide_tactic "Interp" + (function [Tacexp t] -> interp t + | _ -> anomalylabstrm "hide_interp" [<'sTR "Not a tactic AST">]) in + fun ast -> htac [Tacexp ast] + (* For bad tactic calls *) let bad_tactic_args s = anomalylabstrm s diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli index 7d066e8987..9232d598db 100644 --- a/proofs/tacinterp.mli +++ b/proofs/tacinterp.mli @@ -59,7 +59,10 @@ val val_interp : interp_sign -> Coqast.t -> value val interp_tacarg : interp_sign -> Coqast.t -> tactic_arg (* Initial call for interpretation *) -val interp : Coqast.t -> tactic +val interp : Coqast.t -> tactic + +(* Hides interpretation for pretty-print *) +val hide_interp : Coqast.t -> tactic (* For bad tactic calls *) val bad_tactic_args : string -> 'a |