diff options
author | 2008-04-24 11:17:47 +0000 | |
---|---|---|
committer | 2008-04-24 11:17:47 +0000 | |
commit | 57a0e3194660b68c972e084c7f80aa80979c4435 (patch) | |
tree | cf8e9829a1e5732a31e5d1ba7f0621562050e01d /theories/Classes | |
parent | 960efee9230e8aff4817668f918039f768018f09 (diff) |
- 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
Diffstat (limited to 'theories/Classes')
-rw-r--r-- | theories/Classes/Morphisms.v | 20 |
1 files changed, 16 insertions, 4 deletions
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 |