diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-07 16:25:17 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-07 16:25:17 +0000 |
| commit | f2b1574af959529d2881189a91e0d39aea627dc1 (patch) | |
| tree | 7d4cf87fdc8e86ef7fe3dd8ec72e602efd65d05f /proofs | |
| parent | f493b6f2b103dd4e2d0b86acae2fcc7a2b76bdcf (diff) | |
Reparation du pretty-print pour les tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1348 85f007b7-540e-0410-9357-904b9bb8a0f7
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 74fc4fb29..c98840d73 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 7d066e898..9232d598d 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 |