diff options
| author |  Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
| commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
| tree | 0c647056de1832cf1dba5ba58758b9121418e4be /parsing/ppvernac.ml | |
| parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) | |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'parsing/ppvernac.ml')
| -rw-r--r-- | parsing/ppvernac.ml | 13 |
1 files changed, 3 insertions, 10 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index ac2adde2..67cd6f72 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppvernac.ml 11059 2008-06-06 09:29:20Z herbelin $ *) +(* $Id: ppvernac.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Names @@ -403,9 +403,6 @@ let pr_constrarg c = spc () ++ pr_constr c in let pr_lconstrarg c = spc () ++ pr_lconstr c in let pr_intarg n = spc () ++ int n in let pr_lident_constr sep (i,c) = pr_lident i ++ sep ++ pr_constrarg c in -let pr_lname_lident_constr (oi,bk,a) = - (match snd oi with Anonymous -> mt () | Name id -> pr_lident (fst oi, id) ++ spc () ++ str":" ++ spc ()) - ++ pr_lconstr a in let pr_instance_def sep (i,l,c) = pr_lident i ++ prlist_with_sep spc pr_lident l ++ sep ++ pr_constrarg c in @@ -717,8 +714,7 @@ let rec pr_vernac = function | VernacContext l -> hov 1 ( str"Context" ++ spc () ++ str"[" ++ spc () ++ - prlist_with_sep (fun () -> str"," ++ spc()) pr_lname_lident_constr l ++ - spc () ++ str "]") + pr_and_type_binders_arg l ++ spc () ++ str "]") | VernacDeclareInstance id -> @@ -808,10 +804,7 @@ let rec pr_vernac = function (Global.env()) body in hov 1 - (((*if !Flags.p1 then - (if rc then str "Recursive " else mt()) ++ - str "Tactic Definition " else*) - (* Rec by default *) str "Ltac ") ++ + ((str "Ltac ") ++ prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l) | VernacHints (local,dbnames,h) -> pr_hints local dbnames h pr_constr pr_pattern_expr |