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. --- plugins/romega/ReflOmegaCore.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'plugins/romega') diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 36511386a..5e43dfc42 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -1074,16 +1074,19 @@ Qed. avait utilisé le test précédent et fait une elimination dessus. *) Ltac elim_eq_term t1 t2 := + let Aux := fresh "Aux" in pattern (eq_term t1 t2); apply bool_eq_ind; intro Aux; [ generalize (eq_term_true t1 t2 Aux); clear Aux | generalize (eq_term_false t1 t2 Aux); clear Aux ]. Ltac elim_beq t1 t2 := + let Aux := fresh "Aux" in pattern (beq t1 t2); apply bool_eq_ind; intro Aux; [ generalize (beq_true t1 t2 Aux); clear Aux | generalize (beq_false t1 t2 Aux); clear Aux ]. Ltac elim_bgt t1 t2 := + let Aux := fresh "Aux" in pattern (bgt t1 t2); apply bool_eq_ind; intro Aux; [ generalize (bgt_true t1 t2 Aux); clear Aux | generalize (bgt_false t1 t2 Aux); clear Aux ]. -- cgit v1.2.3