From ca318cd0d21ce157a3042b600ded99df6face25e Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 12 Mar 2014 12:21:40 +0100 Subject: 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. --- theories/Classes/CRelationClasses.v | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) (limited to 'theories/Classes') 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. -- cgit v1.2.3