From 4cb7fe525a472928aee02d772458d28a2b71072a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 7 Apr 2014 19:21:05 +0200 Subject: - Fix arity handling in retyping (de Bruijn bug!) - Enforce that no u <= Prop/Set can be added for u introduced by the user in Evd.process_constraints. (Needs to be enforced in the kernel as well, but that's the main entry point). - Fix a test-suite script and remove a regression comment, it's just as before now. --- theories/MSets/MSetGenTree.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/MSets') diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 6164e6e93..2ec125427 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -962,7 +962,7 @@ Proof. firstorder. Qed. Lemma eq_Leq : forall s s', eq s s' <-> L.eq (elements s) (elements s'). Proof. unfold eq, Equal, L.eq; intros. - do 2 setoid_rewrite elements_spec1. (*FIXME due to regression in rewrite *) + setoid_rewrite elements_spec1. firstorder. Qed. -- cgit v1.2.3