factorized tacticals separator and terminator

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 05927a1930a9999cfac9c6f3b5c7058c5946f784..0d539ddbe93cf0c5f450d4fd6fd8c90cde708ed2 100644 (file)
--- 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