diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2014-03-12 12:21:40 +0100 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:57 +0200 |
commit | ca318cd0d21ce157a3042b600ded99df6face25e (patch) | |
tree | ca60f1337c739f46053aa904a1212c209052ef2e /theories/Classes | |
parent | df5e18302e113370906d9ca0b2a2e96dcaccbf0a (diff) |
Fix issue #88: restrict_universe_context was wrongly forgetting about constraints,
and keeping spurious equalities. simplify_universe_context is correct, although
it might keep unused universes around (it's the responsibility of the tactics to
not produce unused universes then).
Add printer for future universe contexts for debugging.
Diffstat (limited to 'theories/Classes')
-rw-r--r-- | theories/Classes/CRelationClasses.v | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v index ca38ac5b4..5e04671ba 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -341,13 +341,14 @@ Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : type (** The partial order defined by subrelation and crelation equivalence. *) -Program Instance subrelation_partial_order : - ! PartialOrder (crelation A) relation_equivalence subrelation. - -Next Obligation. -Proof. - unfold relation_equivalence in *. compute; firstorder. -Qed. +(* Program Instance subrelation_partial_order : *) +(* ! PartialOrder (crelation A) relation_equivalence subrelation. *) +(* Obligation Tactic := idtac. *) + +(* Next Obligation. *) +(* Proof. *) +(* intros x. refine (fun x => x). *) +(* Qed. *) Typeclasses Opaque relation_equivalence. |