From e74526f044f57e77e99c777b5f9354fdd2c74a74 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 28 Jun 2005 09:11:19 +0000 Subject: [PATCH] New argument for LApply: the ident for the generated hypothesis. --- helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 5 +++-- helm/ocaml/cic_transformations/tacticAst.ml | 2 +- helm/ocaml/cic_transformations/tacticAstPp.ml | 7 ++++--- 3 files changed, 8 insertions(+), 6 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 0ef9ec617..0bb6b3222 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -408,8 +408,9 @@ EXTEND let idents = match ident with None -> [] | Some id -> [id] in TacticAst.Intros (loc, Some 1, idents) | IDENT "lapply"; what = tactic_term; - to_what = OPT [ "to" ; t = tactic_term -> t ] -> - TacticAst.LApply (loc, to_what, what) + to_what = OPT [ "to" ; t = tactic_term -> t ]; + ident = OPT [ "using" ; id = IDENT -> id ] -> + TacticAst.LApply (loc, to_what, what, ident) | IDENT "left" -> TacticAst.Left loc | IDENT "letin"; where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> TacticAst.LetIn (loc, t, where) diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 7622ce963..1525cfd8b 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -59,7 +59,7 @@ type ('term, 'ident) tactic = | IdTac of loc | Injection of loc * 'term | Intros of loc * int option * 'ident list - | LApply of loc * 'term option * 'term + | LApply of loc * 'term option * 'term * 'ident option | Left of loc | LetIn of loc * 'term * 'ident | Reduce of loc * reduction_kind * ('term, 'ident) pattern diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 452976e59..bc4346e91 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -119,9 +119,10 @@ 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) + | 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) let pp_flavour = function | `Definition -> "Definition" -- 2.39.2