diff options
Diffstat (limited to 'plugins/romega/ReflOmegaCore.v')
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index b84cf25405..5e43dfc42d 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 ]. @@ -1492,7 +1495,7 @@ with Simplify := match goal with end. Ltac prove_stable x th := - match constr:x with + match constr:(x) with | ?X1 => unfold term_stable, X1; intros; Simplify; simpl; apply th |