From 20641795624dbb03da0401e4dc503660e5e73df6 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 15:50:40 +0100 Subject: 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. --- printing/ppvernac.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'printing/ppvernac.ml') 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) ++ -- cgit v1.2.3