From 9983d0f08f594ddc01700c972d2a2c0f47d32d59 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 10 Feb 2005 15:52:22 +0000 Subject: [PATCH] factorized tacticals separator and terminator --- helm/ocaml/cic_transformations/tacticAstPp.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 05927a193..0d539ddbe 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -27,6 +27,9 @@ open Printf open TacticAst +let tactical_terminator = "." +let tactical_separator = ";" + let pp_term term = CicAstPp.pp_term term let pp_idents idents = "[" ^ String.concat "; " idents ^ "]" @@ -62,6 +65,7 @@ let rec pp_tactic = function | Fourier -> "fourier" | Hint -> "hint" | Injection ident -> "injection " ^ ident + | Intros (None, []) -> "intro" | Intros (num, idents) -> sprintf "intros%s%s" (match num with None -> "" | Some num -> " " ^ string_of_int num) @@ -171,7 +175,8 @@ let rec pp_tactical = function | 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) +and pp_tacticals tacs = + String.concat (tactical_separator ^ " ") (List.map pp_tactical tacs) -let pp_tactical tac = pp_tactical tac ^ "." +let pp_tactical tac = pp_tactical tac ^ tactical_terminator -- 2.39.2