From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 10 Feb 2005 15:52:22 +0000 (+0000)
Subject: factorized tacticals separator and terminator
X-Git-Tag: before_svn_merge~9
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9983d0f08f594ddc01700c972d2a2c0f47d32d59;p=helm.git

factorized tacticals separator and terminator
---

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