From: Stefano Zacchiroli Date: Wed, 18 Feb 2004 14:24:11 +0000 (+0000) Subject: fixed cosmetic typos during pretty printing X-Git-Tag: v0_0_4~148 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=baf82ae86a06877b7e078c91d000aaf6863f8cd1;p=helm.git fixed cosmetic typos during pretty printing --- diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 50ef218f8..5538e7b0f 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -63,7 +63,7 @@ let rec pp_tactic = function | Intros (num, idents) -> sprintf "intros%s%s" (match num with None -> "" | Some num -> " " ^ string_of_int num) - (match idents with [] -> "" | idents -> pp_idents idents) + (match idents with [] -> "" | idents -> " " ^ pp_idents idents) | Left -> "left" | LetIn (term, ident) -> sprintf "let %s in %s" (pp_term term) ident | Reduce (_, _, _) -> assert false (* TODO *) @@ -85,9 +85,11 @@ let rec pp_tactical = function | Repeat tac -> "repeat " ^ pp_tactical tac | Seq tacs -> pp_tacticals tacs | Tactic tac -> pp_tactic tac - | Then (tac, tacs) -> sprintf "%s; [%s]" (pp_tactical tac) (pp_tacticals tacs) + | Then (tac, tacs) -> sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals tacs) | Tries tacs -> sprintf "tries [%s]" (pp_tacticals tacs) | Try tac -> "try " ^ pp_tactical tac and pp_tacticals tacs = String.concat "; " (List.map pp_tactical tacs) +let pp_tactical tac = pp_tactical tac ^ "." +