diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-28 18:29:12 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-29 15:36:54 +0200 |
| commit | adbc03f4ec1fa8d21343fc252b1462b582665aeb (patch) | |
| tree | 0898035aae5310250331cff8a985f1849eaeda49 /theories/Classes | |
| parent | a6ea8b53198fbe6cc1740f8cc84c02b277b1d2ac (diff) | |
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.
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/Morphisms.v | 13 |
1 files changed, 9 insertions, 4 deletions
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 := |