From 2c01bd7b446c1151922ad0a01c3dc6b85f5bea54 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 1 Apr 2016 19:27:30 +0200 Subject: Removing "double induction" from the tactic AST. --- ltac/coretactics.ml4 | 7 +++++++ ltac/tacintern.ml | 4 ---- ltac/tacinterp.ml | 6 ------ ltac/tacsubst.ml | 1 - 4 files changed, 7 insertions(+), 11 deletions(-) (limited to 'ltac') diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index ce28eacc09..63b5463c49 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -222,6 +222,13 @@ TACTIC EXTEND simple_destruct [ "simple" "destruct" quantified_hypothesis(h) ] -> [ Tactics.simple_destruct h ] END +(** Double induction *) + +TACTIC EXTEND double_induction + [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] -> + [ Elim.h_double_induction h1 h2 ] +END + (* Admit *) TACTIC EXTEND admit diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index 3744449e97..0f827755a6 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -520,10 +520,6 @@ let rec intern_atomic lf ist x = Option.map (intern_or_and_intro_pattern_loc lf ist) ipats), Option.map (clause_app (intern_hyp_location ist)) cls)) l, Option.map (intern_constr_with_bindings ist) el)) - | TacDoubleInduction (h1,h2) -> - let h1 = intern_quantified_hypothesis ist h1 in - let h2 = intern_quantified_hypothesis ist h2 in - TacDoubleInduction (h1,h2) (* Context management *) | TacRename l -> TacRename (List.map (fun (id1,id2) -> diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index fcc29a8302..f6f988ee23 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1822,12 +1822,6 @@ and interp_atomic ist tac : unit Proofview.tactic = in Sigma.Unsafe.of_pair (tac, sigma) end } - | TacDoubleInduction (h1,h2) -> - let h1 = interp_quantified_hypothesis ist h1 in - let h2 = interp_quantified_hypothesis ist h2 in - name_atomic - (TacDoubleInduction (h1,h2)) - (Elim.h_double_induction h1 h2) (* Context management *) | TacRename l -> Proofview.Goal.enter { enter = begin fun gl -> diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index 3f504b7f37..71dd718e87 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -162,7 +162,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with subst_induction_arg subst c, ids, cls) l in let el' = Option.map (subst_glob_with_bindings subst) el in TacInductionDestruct (isrec,ev,(l',el')) - | TacDoubleInduction (h1,h2) as x -> x (* Context management *) | TacRename l as x -> x -- cgit v1.2.3 From 64637ffc5054199459d9fc7f07b84a99da71c6f1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 17:24:05 +0100 Subject: Removing "intro" from the tactic AST. Note that this breaks the compatibility, in a beneficial way I believe. Tactics defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction on a local identifier anymore. They must use the "fresh" primitive instead. --- ltac/coretactics.ml4 | 14 +++++++++++++- ltac/tacintern.ml | 3 --- ltac/tacinterp.ml | 10 ---------- ltac/tacsubst.ml | 1 - 4 files changed, 13 insertions(+), 15 deletions(-) (limited to 'ltac') diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 63b5463c49..efabdc4ad7 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -197,6 +197,19 @@ TACTIC EXTEND intros_until [ "intros" "until" quantified_hypothesis(h) ] -> [ Tactics.intros_until h ] END +TACTIC EXTEND intro +| [ "intro" ] -> [ Tactics.intro_move None MoveLast ] +| [ "intro" ident(id) ] -> [ Tactics.intro_move (Some id) MoveLast ] +| [ "intro" ident(id) "at" "top" ] -> [ Tactics.intro_move (Some id) MoveFirst ] +| [ "intro" ident(id) "at" "bottom" ] -> [ Tactics.intro_move (Some id) MoveLast ] +| [ "intro" ident(id) "after" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveAfter h) ] +| [ "intro" ident(id) "before" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveBefore h) ] +| [ "intro" "at" "top" ] -> [ Tactics.intro_move None MoveFirst ] +| [ "intro" "at" "bottom" ] -> [ Tactics.intro_move None MoveLast ] +| [ "intro" "after" hyp(h) ] -> [ Tactics.intro_move None (MoveAfter h) ] +| [ "intro" "before" hyp(h) ] -> [ Tactics.intro_move None (MoveBefore h) ] +END + (** Move *) TACTIC EXTEND move @@ -287,7 +300,6 @@ let initial_atomic () = "hnf", TacReduce(Hnf,nocl); "simpl", TacReduce(Simpl (Redops.all_flags,None),nocl); "compute", TacReduce(Cbv Redops.all_flags,nocl); - "intro", TacIntroMove(None,MoveLast); "intros", TacIntroPattern []; ] in diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index 0f827755a6..bd48ffb723 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -481,9 +481,6 @@ let rec intern_atomic lf ist x = (* Basic tactics *) | TacIntroPattern l -> TacIntroPattern (List.map (intern_intro_pattern lf ist) l) - | TacIntroMove (ido,hto) -> - TacIntroMove (Option.map (intern_ident lf ist) ido, - intern_move_location ist hto) | TacExact c -> TacExact (intern_constr ist c) | TacApply (a,ev,cb,inhyp) -> TacApply (a,ev,List.map (intern_constr_with_bindings_arg ist) cb, diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index f6f988ee23..c8fa9367f3 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1644,16 +1644,6 @@ and interp_atomic ist tac : unit Proofview.tactic = expected behaviour. *) (Tactics.intro_patterns l')) sigma end } - | TacIntroMove (ido,hto) -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = project gl in - let mloc = interp_move_location ist env sigma hto in - let ido = Option.map (interp_ident ist env sigma) ido in - name_atomic ~env - (TacIntroMove(ido,mloc)) - (Tactics.intro_move ido mloc) - end } | TacExact c -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"") begin diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index 71dd718e87..1e974d6f5d 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -137,7 +137,6 @@ let rec subst_match_goal_hyps subst = function let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Basic tactics *) | TacIntroPattern l -> TacIntroPattern (List.map (subst_intro_pattern subst) l) - | TacIntroMove _ as x -> x | TacExact c -> TacExact (subst_glob_constr subst c) | TacApply (a,ev,cb,cl) -> TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,cl) -- cgit v1.2.3 From 5cd0310f061b5eb1a631a0fff0ee7eb9674a11c3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 Apr 2016 14:13:14 +0200 Subject: Removing "exact" from the tactic AST. --- ltac/coretactics.ml4 | 4 ++++ ltac/extraargs.ml4 | 11 +++++++++++ ltac/extraargs.mli | 5 +++++ ltac/tacintern.ml | 1 - ltac/tacinterp.ml | 12 ------------ ltac/tacinterp.mli | 3 +++ ltac/tacsubst.ml | 1 - 7 files changed, 23 insertions(+), 14 deletions(-) (limited to 'ltac') diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index efabdc4ad7..8e37653f57 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -26,6 +26,10 @@ TACTIC EXTEND reflexivity [ "reflexivity" ] -> [ Tactics.intros_reflexivity ] END +TACTIC EXTEND exact + [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ] +END + TACTIC EXTEND assumption [ "assumption" ] -> [ Tactics.assumption ] END diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index 0bddcc9fdd..9a2a176cbf 100644 --- a/ltac/extraargs.ml4 +++ b/ltac/extraargs.ml4 @@ -15,6 +15,7 @@ open Constrarg open Pcoq.Prim open Pcoq.Constr open Names +open Tacmach open Tacexpr open Taccoerce open Tacinterp @@ -175,6 +176,16 @@ ARGUMENT EXTEND lglob [ lconstr(c) ] -> [ c ] END +let interp_casted_constr ist gl c = + interp_constr_gen (Pretyping.OfType (pf_concl gl)) ist (pf_env gl) (project gl) c + +ARGUMENT EXTEND casted_constr + TYPED AS constr + PRINTED BY pr_gen + INTERPRETED BY interp_casted_constr + [ constr(c) ] -> [ c ] +END + type 'id gen_place= ('id * hyp_location_flag,unit) location type loc_place = Id.t Loc.located gen_place diff --git a/ltac/extraargs.mli b/ltac/extraargs.mli index 4d1d8ba7fe..2118e87b11 100644 --- a/ltac/extraargs.mli +++ b/ltac/extraargs.mli @@ -38,6 +38,11 @@ val wit_lconstr : Tacexpr.glob_constr_and_expr, Constr.t) Genarg.genarg_type +val wit_casted_constr : + (constr_expr, + Tacexpr.glob_constr_and_expr, + Constr.t) Genarg.genarg_type + val glob : constr_expr Pcoq.Gram.entry val lglob : constr_expr Pcoq.Gram.entry diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index bd48ffb723..c1c7be1cc9 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -481,7 +481,6 @@ let rec intern_atomic lf ist x = (* Basic tactics *) | TacIntroPattern l -> TacIntroPattern (List.map (intern_intro_pattern lf ist) l) - | TacExact c -> TacExact (intern_constr ist c) | TacApply (a,ev,cb,inhyp) -> TacApply (a,ev,List.map (intern_constr_with_bindings_arg ist) cb, Option.map (intern_in_hyp_as ist lf) inhyp) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index c8fa9367f3..c51c36538d 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -684,10 +684,6 @@ let interp_typed_pattern ist env sigma (_,c,_) = interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in pattern_of_constr env sigma c -(* Interprets a constr expression casted by the current goal *) -let pf_interp_casted_constr ist gl c = - interp_constr_gen (OfType (pf_concl gl)) ist (pf_env gl) (project gl) c - (* Interprets a constr expression *) let pf_interp_constr ist gl = interp_constr ist (pf_env gl) (project gl) @@ -1644,14 +1640,6 @@ and interp_atomic ist tac : unit Proofview.tactic = expected behaviour. *) (Tactics.intro_patterns l')) sigma end } - | TacExact c -> - (* spiwack: until the tactic is in the monad *) - Proofview.Trace.name_tactic (fun () -> Pp.str"") begin - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> - let (sigma, c_interp) = pf_interp_casted_constr ist gl c in - Sigma.Unsafe.of_pair (Tactics.exact_no_check c_interp, sigma) - end } - end | TacApply (a,ev,cb,cl) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"") begin diff --git a/ltac/tacinterp.mli b/ltac/tacinterp.mli index 8bb6ee4cdf..6f64981eff 100644 --- a/ltac/tacinterp.mli +++ b/ltac/tacinterp.mli @@ -72,6 +72,9 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map -> Id.t Loc.located -> Id.t +val interp_constr_gen : Pretyping.typing_constraint -> interp_sign -> + Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Evd.evar_map * constr + val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr bindings -> Evd.evar_map * constr bindings diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index 1e974d6f5d..3c1a384ceb 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -137,7 +137,6 @@ let rec subst_match_goal_hyps subst = function let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Basic tactics *) | TacIntroPattern l -> TacIntroPattern (List.map (subst_intro_pattern subst) l) - | TacExact c -> TacExact (subst_glob_constr subst c) | TacApply (a,ev,cb,cl) -> TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,cl) | TacElim (ev,cb,cbo) -> -- cgit v1.2.3 From 3206bf597d63066d9d9f8adfd0fe76e3c1c97e4d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 9 May 2016 00:12:19 +0200 Subject: Removing "rename" from the tactic AST. --- ltac/coretactics.ml4 | 6 ++++++ ltac/extraargs.ml4 | 8 ++++++++ ltac/extraargs.mli | 2 ++ ltac/tacintern.ml | 6 ------ ltac/tacinterp.ml | 14 -------------- ltac/tacsubst.ml | 3 --- 6 files changed, 16 insertions(+), 23 deletions(-) (limited to 'ltac') diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 8e37653f57..9879cfc280 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -223,6 +223,12 @@ TACTIC EXTEND move | [ "move" hyp(id) "before" hyp(h) ] -> [ Tactics.move_hyp id (MoveBefore h) ] END +(** Rename *) + +TACTIC EXTEND rename +| [ "rename" ne_rename_list_sep(ids, ",") ] -> [ Tactics.rename_hyp ids ] +END + (** Revert *) TACTIC EXTEND revert diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index 9a2a176cbf..e6d0a9c69c 100644 --- a/ltac/extraargs.ml4 +++ b/ltac/extraargs.ml4 @@ -236,6 +236,14 @@ ARGUMENT EXTEND hloc END +let pr_rename _ _ _ (n, m) = Nameops.pr_id n ++ str " into " ++ Nameops.pr_id m + +ARGUMENT EXTEND rename + TYPED AS ident * ident + PRINTED BY pr_rename +| [ ident(n) "into" ident(m) ] -> [ (n, m) ] +END + (* Julien: Mise en commun des differentes version de replace with in by *) let pr_by_arg_tac _prc _prlc prtac opt_c = diff --git a/ltac/extraargs.mli b/ltac/extraargs.mli index 2118e87b11..0cf77935c2 100644 --- a/ltac/extraargs.mli +++ b/ltac/extraargs.mli @@ -16,6 +16,8 @@ val wit_orient : bool Genarg.uniform_genarg_type val orient : bool Pcoq.Gram.entry val pr_orient : bool -> Pp.std_ppcmds +val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type + val occurrences : (int list or_var) Pcoq.Gram.entry val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type val pr_occurrences : int list or_var -> Pp.std_ppcmds diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index c1c7be1cc9..d39f835528 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -516,12 +516,6 @@ let rec intern_atomic lf ist x = Option.map (intern_or_and_intro_pattern_loc lf ist) ipats), Option.map (clause_app (intern_hyp_location ist)) cls)) l, Option.map (intern_constr_with_bindings ist) el)) - (* Context management *) - | TacRename l -> - TacRename (List.map (fun (id1,id2) -> - intern_hyp ist id1, - intern_hyp ist id2) l) - (* Conversion *) | TacReduce (r,cl) -> dump_glob_red_expr r; diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index c51c36538d..5ee9b0fc4d 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1800,20 +1800,6 @@ and interp_atomic ist tac : unit Proofview.tactic = in Sigma.Unsafe.of_pair (tac, sigma) end } - (* Context management *) - | TacRename l -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = pf_env gl in - let sigma = project gl in - let l = - List.map (fun (id1,id2) -> - interp_hyp ist env sigma id1, - interp_ident ist env sigma (snd id2)) l - in - name_atomic ~env - (TacRename l) - (Tactics.rename_hyp l) - end } (* Conversion *) | TacReduce (r,cl) -> diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index 3c1a384ceb..2c3c76ef74 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -161,9 +161,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with let el' = Option.map (subst_glob_with_bindings subst) el in TacInductionDestruct (isrec,ev,(l',el')) - (* Context management *) - | TacRename l as x -> x - (* Conversion *) | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl) | TacChange (op,c,cl) -> -- cgit v1.2.3