From 2de8910d2cc0af096e6d91b0ea165997ce144503 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 2 May 2014 11:34:53 +0200 Subject: - Fix treatment of global universe constraints which should be passed along in the Evd of proofs (Evd.from_env). - Allow to set the Store.t value of new evars, e.g. to set constraint evars as unresolvable in rewrite.ml. - Fix a HUGE performance problem in the processing of constraints, which was remerging all the previous constraints with the ambient global universes at each new constraint addition. Performance is now back to (or better than) normal. --- theories/Numbers/NatInt/NZGcd.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/Numbers') diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v index d7e598fb4..e4e1fe3b0 100644 --- a/theories/Numbers/NatInt/NZGcd.v +++ b/theories/Numbers/NatInt/NZGcd.v @@ -107,8 +107,8 @@ Proof. now rewrite Hr, Hq, mul_assoc. Qed. -Instance divide_reflexive : Reflexive divide := divide_refl. -Instance divide_transitive : Transitive divide := divide_trans. +Instance divide_reflexive : Reflexive divide | 5 := divide_refl. +Instance divide_transitive : Transitive divide | 5 := divide_trans. (** Due to sign, no general antisymmetry result *) -- cgit v1.2.3