From: Stefano Zacchiroli Date: Mon, 23 Feb 2004 16:04:41 +0000 (+0000) Subject: added a space between term and "using" keyword X-Git-Tag: v0_0_4~101 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=84d34593eea96fc1eb273ffd3b67c4e32a7c1dc9;p=helm.git added a space between term and "using" keyword --- diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 5538e7b0f..6627c4613 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -52,7 +52,7 @@ let rec pp_tactic = function | Discriminate ident -> "discriminate " ^ ident | Elim (term, using) -> sprintf "elim " ^ pp_term term ^ - (match using with None -> "" | Some term -> "using " ^ pp_term term) + (match using with None -> "" | Some term -> " using " ^ pp_term term) | ElimType term -> "elim type " ^ pp_term term | Exact term -> "exact " ^ pp_term term | Exists -> "exists"