diff options
| author |  gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-06-13 16:05:01 +0000 |
|---|---|---|
| committer | gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-06-13 16:05:01 +0000 |
| commit | 6bfee526ff8266b120cb413745bdc4adcd7d0425 (patch) | |
| tree | 93fc326825ef8c16b9c389ae9d3a469d431e5739 /parsing | |
| parent | 3863d2c8a005cf1b96ffded26b333ed8e345f530 (diff) | |
Petits beug d'affichages.
Benj
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2778 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pptactic.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 9dc447f7d..87ac8e3ba 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -101,7 +101,7 @@ let pr_with_bindings prc (c,bl) = prc c ++ hv 0 (pr_bindings prc bl) let rec pr_intro_pattern = function | IntroOrAndPattern pll -> str "[" ++ - hv 0 (prlist_with_sep pr_coma (prlist_with_sep spc pr_intro_pattern) pll) + hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll) ++ str "]" (* | IntroAndPattern pl -> @@ -229,7 +229,7 @@ let rec pr_rawgen prtac x = with Not_found -> str " [no printer for " ++ str s ++ str "] " let rec pr_raw_tacarg_using_rule pr_gen = function - | Egrammar.TacTerm s :: l, al -> str s ++ pr_raw_tacarg_using_rule pr_gen (l,al) + | Egrammar.TacTerm s :: l, al -> spc () ++ str s ++ pr_raw_tacarg_using_rule pr_gen (l,al) | Egrammar.TacNonTerm _ :: l, a :: al -> pr_gen a ++ pr_raw_tacarg_using_rule pr_gen (l,al) | [], [] -> mt () | _ -> failwith "Inconsistent arguments of extended tactic" @@ -286,7 +286,7 @@ let rec pr_generic prtac x = with Not_found -> str "[no printer for " ++ str s ++ str "]" let rec pr_tacarg_using_rule prt = function - | Egrammar.TacTerm s :: l, al -> str s ++ pr_tacarg_using_rule prt (l,al) + | Egrammar.TacTerm s :: l, al -> spc () ++ str s ++ pr_tacarg_using_rule prt (l,al) | Egrammar.TacNonTerm _ :: l, a :: al -> pr_generic prt a ++ pr_tacarg_using_rule prt (l,al) | [], [] -> mt () | _ -> failwith "Inconsistent arguments of extended tactic" @@ -327,7 +327,7 @@ and pr_atom1 = function (* Basic tactics *) | TacIntroPattern [] as t -> pr_atom0 t | TacIntroPattern (_::_ as p) -> - hov 1 (str "Intro" ++ spc () ++ prlist_with_sep spc pr_intro_pattern p) + hov 1 (str "Intros" ++ spc () ++ prlist_with_sep spc pr_intro_pattern p) | TacIntrosUntil h -> hv 1 (str "Intros until" ++ pr_arg pr_quantified_hypothesis h) | TacIntroMove (None,None) as t -> pr_atom0 t |