From d223f85d0fd57ce74dcdcc8690a36f1ef87b408d Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 21 Mar 2013 19:13:04 +0000 Subject: Using hnf instead of "intro H" for forcing reduction to a product. Added full betaiota in hnf. This seems more natural, even if it changes the strict meaning of hnf. This is source of incompatibilities as "intro" might succeed more often. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16338 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Classes/Morphisms_Prop.v | 12 ------------ 1 file changed, 12 deletions(-) (limited to 'theories/Classes') diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v index 2252e42fc..6f02ac9f5 100644 --- a/theories/Classes/Morphisms_Prop.v +++ b/theories/Classes/Morphisms_Prop.v @@ -93,21 +93,9 @@ Program Instance all_iff_morphism {A : Type} : Program Instance all_impl_morphism {A : Type} : Proper (pointwise_relation A impl ==> impl) (@all A) | 1. - Next Obligation. - Proof. - unfold pointwise_relation, all in *. - intuition ; specialize (H x0) ; intuition. - Qed. - Program Instance all_inverse_impl_morphism {A : Type} : Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@all A) | 1. - Next Obligation. - Proof. - unfold pointwise_relation, all in *. - intuition ; specialize (H x0) ; intuition. - Qed. - (** Equivalent points are simultaneously accessible or not *) Instance Acc_pt_morphism {A:Type}(E R : A->A->Prop) -- cgit v1.2.3