diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-16 15:50:40 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-18 15:58:43 +0100 |
| commit | 20641795624dbb03da0401e4dc503660e5e73df6 (patch) | |
| tree | 3e4a94692a2c7ec1c722e8a8a3db94783a4cd684 /printing/ppvernac.ml | |
| parent | 84f54fd0923c15109910123443348c193e37fe0f (diff) | |
CLEANUP: Vernacexpr.VernacDeclareTacticDefinition
The definition of Vernacexpr.VernacDeclareTacticDefinition was changed.
The original definition allowed us to represent non-sensical value such as:
VernacDeclareTacticDefinition(Qualid ..., false, ...)
The new definition prevents that.
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 5110cf7b2..f216c599d 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1031,12 +1031,17 @@ module Make (* Commands *) | VernacDeclareTacticDefinition l -> - let pr_tac_body (id, redef, body) = + let pr_tac_body tacdef_body = + let id, redef, body = + match tacdef_body with + | TacticDefinition ((_,id), body) -> str (Id.to_string 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 - pr_ltac_ref id ++ + id ++ prlist (function None -> str " _" | Some id -> spc () ++ pr_id id) idl ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++ |