From 7b78ae643999aa95b95b376fab54adb33dbed206 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 28 Jun 2005 17:38:42 +0000 Subject: [PATCH] lapply improved --- 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 ee099e420..2e8124d7e 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -122,7 +122,7 @@ let rec pp_tactic = function | LApply (_, term_opt, term, ident) -> sprintf "lapply %s%s%s" (pp_term_ast term) (match term_opt with None -> "" | Some t -> " to " ^ pp_term_ast t) - (match ident with None -> "" | Some id -> " " ^ id) + (match ident with None -> "" | Some id -> " using " ^ id) let pp_flavour = function | `Definition -> "Definition" -- 2.39.2