From 5f57966efd85fb295701f06fd0488e9fe1bbb99f Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 4 May 2004 10:45:54 +0000 Subject: [PATCH] removed traliling dot in command pretty printer, now it's added by the tactical pp --- helm/ocaml/cic_transformations/tacticAstPp.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 9a544234d..5c96b64d3 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -86,14 +86,14 @@ let pp_flavour = function | `Theorem -> "Theorem" let pp_command = function - | Abort -> "Abort." - | Check term -> sprintf "Check %s." (CicAstPp.pp_term term) - | Proof -> "Proof." + | Abort -> "Abort" + | Check term -> sprintf "Check %s" (CicAstPp.pp_term term) + | Proof -> "Proof" | Qed name -> - (match name with None -> "Qed." | Some name -> sprintf "Save %s." name) - | Quit -> "Quit." + (match name with None -> "Qed" | Some name -> sprintf "Save %s" name) + | Quit -> "Quit" | Theorem (flavour, name, typ, body) -> - sprintf "%s %s: %s %s." + sprintf "%s %s: %s %s" (pp_flavour flavour) (match name with None -> "" | Some name -> name) (CicAstPp.pp_term typ) -- 2.39.2