diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-07 18:02:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-08 15:52:56 +0200 |
| commit | dfac5aa2285de5b89f08ada3c30c0a1594737440 (patch) | |
| tree | 37fa3f3481d03c4a777595e1ec0eab631cd528aa /printing | |
| parent | 13266ce4c37cb648b5e4e391aa5d7486bbcdb4ee (diff) | |
Making Vernacexpr independent from Tacexpr.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 40ce28dc0..d4de05da8 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -195,7 +195,7 @@ module Make | HintsExtern (n,c,tac) -> let pat = match c with None -> mt () | Some pat -> pr_pat pat in keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++ - spc() ++ pr_raw_tactic tac + spc() ++ pr_raw_generic (Global.env ()) tac in hov 2 (keyword "Hint "++ pph ++ opth) @@ -1179,12 +1179,12 @@ module Make return (keyword "Proof " ++ spc () ++ keyword "using" ++ spc() ++ pr_using e) | VernacProof (Some te, None) -> - return (keyword "Proof with" ++ spc() ++ pr_raw_tactic te) + return (keyword "Proof with" ++ spc() ++ pr_raw_generic (Global.env ()) te) | VernacProof (Some te, Some e) -> return ( keyword "Proof" ++ spc () ++ keyword "using" ++ spc() ++ pr_using e ++ spc() ++ - keyword "with" ++ spc() ++pr_raw_tactic te + keyword "with" ++ spc() ++ pr_raw_generic (Global.env ()) te ) | VernacProofMode s -> return (keyword "Proof Mode" ++ str s) |