From aa0c24992572f26d8e78ae34b60c7e151167cf49 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 27 Jun 2005 08:16:24 +0000 Subject: [PATCH] fixed LApply pretty printing --- helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 5 +++-- helm/ocaml/cic_transformations/tacticAstPp.ml | 3 +++ helm/ocaml/tactics/autoTactic.ml | 2 +- 3 files changed, 7 insertions(+), 3 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 9a88a2cbe..d3d6e28ae 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -417,8 +417,9 @@ EXTEND TacticAst.Transitivity (loc, t) | [ IDENT "fwd" ]; t = term -> TacticAst.FwdSimpl (loc, t) - | [ IDENT "lapply" ]; what = tactic_term; to_what = OPT [ "to" ; t = tactic_term -> t ] -> - TacticAst.LApply (loc, to_what, what) + | [ IDENT "lapply" ]; what = tactic_term; + to_what = OPT [ "to" ; t = tactic_term -> t ] -> + TacticAst.LApply (loc, to_what, what) ] ]; tactical: diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 263382ef1..f916a2b86 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -119,6 +119,9 @@ let rec pp_tactic = function | Symmetry _ -> "symmetry" | Transitivity (_, term) -> "transitivity " ^ pp_term_ast term | FwdSimpl (_, term) -> sprintf "fwd %s" (pp_term_ast term) + | LApply (_, term_opt, term) -> + sprintf "lapply %s%s" (pp_term_ast term) + (match term_opt with | None -> "" | Some t -> " to " ^ pp_term_ast t) let pp_flavour = function | `Definition -> "Definition" diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml index c7cdc97ac..ea29499a4 100644 --- a/helm/ocaml/tactics/autoTactic.ml +++ b/helm/ocaml/tactics/autoTactic.ml @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) - let debug_print = prerr_endline + let debug_print = ignore (*prerr_endline *) (* let debug_print = fun _ -> () *) -- 2.39.2