aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-04-24 11:17:47 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-04-24 11:17:47 +0000
commit57a0e3194660b68c972e084c7f80aa80979c4435 (patch)
treecf8e9829a1e5732a31e5d1ba7f0621562050e01d /theories/Classes
parent960efee9230e8aff4817668f918039f768018f09 (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.v20
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