Permalink
Browse files

Fixing Show Script issues.

Author: Daniel de Rauglaudre

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15821 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent b5c67e4 commit 5e8ebbc13909125093e2c7aa18e00cf30cad6362 ppedrot committed Sep 20, 2012
Showing with 13 additions and 6 deletions.
  1. +12 −5 printing/pptactic.ml
  2. +1 −1 tactics/extraargs.ml4
View
@@ -263,7 +263,14 @@ let rec pr_generic prc prlc prtac prpat x =
let rec tacarg_using_rule_token pr_gen = function
| Some s :: l, al -> str s :: tacarg_using_rule_token pr_gen (l,al)
- | None :: l, a :: al -> pr_gen a :: tacarg_using_rule_token pr_gen (l,al)
+ | None :: l, a :: al ->
+ let print_it =
+ match genarg_tag a with
+ | OptArgType _ -> fold_opt (fun _ -> true) false a
+ | _ -> true
+ in
+ let r = tacarg_using_rule_token pr_gen (l,al) in
+ if print_it then pr_gen a :: r else r
| [], [] -> []
| _ -> failwith "Inconsistent arguments of extended tactic"
@@ -422,7 +429,7 @@ let pr_clauses default_is_concl pr_id = function
(if occs = NoOccurrences then mt ()
else pr_with_occurrences (fun () -> str" |- *") (occs,())))
-let pr_orient b = if b then mt () else str " <-"
+let pr_orient b = if b then mt () else str "<- "
let pr_multi = function
| Precisely 1 -> mt ()
@@ -804,17 +811,17 @@ and pr_atom1 = function
(* Equivalence relations *)
| TacReflexivity as x -> pr_atom0 x
- | TacSymmetry cls -> str "symmetry " ++ pr_clauses (Some true) pr_ident cls
+ | TacSymmetry cls -> str "symmetry" ++ pr_clauses (Some true) pr_ident cls
| TacTransitivity (Some c) -> str "transitivity" ++ pr_constrarg c
| TacTransitivity None -> str "etransitivity"
(* Equality and inversion *)
| TacRewrite (ev,l,cl,by) ->
- hov 1 (str (with_evars ev "rewrite") ++
+ hov 1 (str (with_evars ev "rewrite") ++ spc () ++
prlist_with_sep
(fun () -> str ","++spc())
(fun (b,m,c) ->
- pr_orient b ++ spc() ++ pr_multi m ++ pr_with_bindings c)
+ pr_orient b ++ pr_multi m ++ pr_with_bindings c)
l
++ pr_clauses (Some true) pr_ident cl
++ (match by with Some by -> pr_by_tactic (pr_tac_level ltop) by | None -> mt()))
View
@@ -204,7 +204,7 @@ let pr_in_hyp pr_id (lo,concl) : Pp.std_ppcmds =
| None,false -> str "in" ++ spc () ++ str "*" ++ spc () ++ str "|-"
| Some l,_ ->
str "in" ++
- pr_sequence pr_id l ++
+ spc () ++ prlist_with_sep pr_comma pr_id l ++
match concl with
| true -> spc () ++ str "|-" ++ spc () ++ str "*"
| _ -> mt ()

0 comments on commit 5e8ebbc

Please sign in to comment.