From adbc03f4ec1fa8d21343fc252b1462b582665aeb Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 28 Jun 2014 18:29:12 +0200 Subject: Move Params definition in generalize rewriting out of a section so that its universe doesn't get constrained unnecessarily (bug found in MathClasse). Also avoid using rewrite itself in a proof in Morphisms. --- theories/Classes/Morphisms.v | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) (limited to 'theories/Classes') diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 921f21233..1560d8a31 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -417,8 +417,6 @@ Section GenericInstances. Proper R' (m x). Proof. simpl_relation. Qed. - Class Params (of : A) (arity : nat). - Lemma flip_respectful (R : relation A) (R' : relation B) : relation_equivalence (flip (R ==> R')) (flip R ==> flip R'). Proof. @@ -461,6 +459,8 @@ Class PartialApplication. CoInductive normalization_done : Prop := did_normalization. +Class Params {A : Type} (of : A) (arity : nat). + Ltac partial_application_tactic := let rec do_partial_apps H m cont := match m with @@ -563,11 +563,16 @@ Section Normalize. End Normalize. -Lemma flip_arrow `(NA : Normalizes A R (flip R'''), NB : Normalizes B R' (flip R'')) : +Lemma flip_arrow {A : Type} {B : Type} + `(NA : Normalizes A R (flip R'''), NB : Normalizes B R' (flip R'')) : Normalizes (A -> B) (R ==> R') (flip (R''' ==> R'')%signature). Proof. unfold Normalizes in *. intros. - rewrite NA, NB. firstorder. + unfold relation_equivalence in *. + unfold predicate_equivalence in *. simpl in *. + unfold respectful. unfold flip in *. firstorder. + apply NB. apply H. apply NA. apply H0. + apply NB. apply H. apply NA. apply H0. Qed. Ltac normalizes := -- cgit v1.2.3