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.

---
 tactics/rewrite.ml | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index dc9cc471c2..9dd6c941ee 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -120,8 +120,10 @@ let goalevars evars = fst evars
 let cstrevars evars = snd evars
 
 let new_cstr_evar (evd,cstrs) env t =
-  let evd', t = Evarutil.new_evar evd env t in
-    (evd', Evar.Set.add (fst (destEvar t)) cstrs), t
+  let s = Typeclasses.set_resolvable Evd.Store.empty false in
+  let evd', t = Evarutil.new_evar ~store:s evd env t in
+  let ev, _ = destEvar t in
+    (evd', Evar.Set.add ev cstrs), t
 
 (** Building or looking up instances. *)
 let e_new_cstr_evar evars env t =
@@ -602,6 +604,9 @@ let shrink_evd sigma ext =
 let no_constraints cstrs = 
   fun ev _ -> not (Evar.Set.mem ev cstrs)
 
+let all_constraints cstrs = 
+  fun ev _ -> Evar.Set.mem ev cstrs
+
 let poly_inverse sort =
   if sort then PropGlobal.inverse else TypeGlobal.inverse
 
@@ -641,7 +646,7 @@ let unify_eqn env (sigma, cstrs) hypinfo by t =
 	       (* 	  env'.evd, prf, c1, c2, car, rel) *)
 	    else raise Reduction.NotConvertible
     in
-    let evars = evd', Evar.Set.empty in
+    let evars = evd', cstrs in
     let evd, res =
       if l2r then evars, (prf, (car, rel, c1, c2))
       else
@@ -1332,7 +1337,8 @@ let apply_strategy (s : strategy) env avoid concl (prop, cstr) evars =
 	Some (Some (res.rew_prf, res.rew_evars, res.rew_car, res.rew_from, res.rew_to))
 
 let solve_constraints env (evars,cstrs) =
-  Typeclasses.resolve_typeclasses env ~split:false ~fail:true evars
+  Typeclasses.resolve_typeclasses env ~split:false ~fail:true 
+    (Typeclasses.mark_resolvables ~filter:(all_constraints cstrs) evars)
 
 let nf_zeta =
   Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
-- 
cgit v1.2.3