From 84d34593eea96fc1eb273ffd3b67c4e32a7c1dc9 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 23 Feb 2004 16:04:41 +0000 Subject: [PATCH] added a space between term and "using" keyword --- helm/ocaml/cic_transformations/tacticAstPp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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" -- 2.39.2