diff options
| author | Pierre-Marie Pédrot | 2016-03-20 02:23:21 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-20 02:41:58 +0100 |
| commit | 4f52bd681ad9bbcbbd68406a58b47d8e962336ed (patch) | |
| tree | 5b891de8b42d9cb20ec3273ae1e02bd586f42fd0 /printing | |
| parent | 9f5d9cd2622f3890e70dad01898868fe29df6048 (diff) | |
Moving the Ltac definition command to an EXTEND based command.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 23 |
1 files changed, 0 insertions, 23 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index edd32e8337..c1f5e122bd 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -995,29 +995,6 @@ module Make return (keyword "Cd" ++ pr_opt qs s) (* Commands *) - | VernacDeclareTacticDefinition l -> - let pr_tac_body tacdef_body = - let id, redef, body = - match tacdef_body with - | TacticDefinition ((_,id), body) -> pr_id id, false, body - | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body - in - let idl, body = - match body with - | Tacexpr.TacFun (idl,b) -> idl,b - | _ -> [], body in - id ++ - prlist (function None -> str " _" - | Some id -> spc () ++ pr_id id) idl - ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++ - pr_raw_tactic body - in - return ( - hov 1 - (keyword "Ltac" ++ spc () ++ - prlist_with_sep (fun () -> - fnl() ++ keyword "with" ++ spc ()) pr_tac_body l) - ) | VernacCreateHintDb (dbname,b) -> return ( hov 1 (keyword "Create HintDb" ++ spc () ++ |