From 57a0e3194660b68c972e084c7f80aa80979c4435 Mon Sep 17 00:00:00 2001 From: msozeau Date: Thu, 24 Apr 2008 11:17:47 +0000 Subject: - Add pretty-printers for Idpred, Cpred and transparent_state, used for debugging and printing hint databases - Typeclasses unfold now correctly adds _global_ unfold hints. - New tactic autosimpl to do simplification using the declared unfold hints in given hint databases. - Work on auto-modulo-some-delta (the declared Unfold constants), actually used mostly if the goal contains evars, as Hint_db.map_auto does not work up-to any conversions (yet). - Fix GenMul which was using the old semantics of failing early because of variance checks, which is not possible in the new implementation. - Restrict when reflexive_morphism may be used using an extern tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10842 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Classes/Morphisms.v | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) (limited to 'theories/Classes') diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index e2d3f21c7..4b5b71a19 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -334,10 +334,6 @@ Proof. firstorder. Qed. (* eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *) (* Proof. simpl_relation. Qed. *) -Instance [ Reflexive A R ] (x : A) => - reflexive_morphism : Morphism R x | 4. -Proof. firstorder. Qed. - (** [R] is Reflexive, hence we can build the needed proof. *) Program Instance [ Morphism (A -> B) (R ==> R') m, MorphismProxy A R x ] => @@ -407,8 +403,24 @@ Inductive normalization_done : Prop := did_normalization. Ltac morphism_normalization := match goal with | [ _ : normalization_done |- _ ] => fail +(* | [ _ : subrelation_done |- _ ] => fail (* avoid useless interleavings. *) *) | [ |- @Morphism _ _ _ ] => let H := fresh "H" in set(H:=did_normalization) ; eapply @morphism_releq_morphism end. Hint Extern 5 (@Morphism _ _ _) => morphism_normalization : typeclass_instances. + +(** Every reflexive relation gives rise to a morphism, only for immediately solving goals without variables. *) + +Lemma reflexive_morphism [ Reflexive A R ] (x : A) + : Morphism R x. +Proof. firstorder. Qed. + +Ltac morphism_reflexive := + match goal with + | [ _ : normalization_done |- _ ] => fail + | [ _ : subrelation_done |- _ ] => fail + | [ |- @Morphism _ _ _ ] => eapply @reflexive_morphism + end. + +Hint Extern 4 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances. \ No newline at end of file -- cgit v1.2.3