- 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.

1 files changed, 10 insertions, 4 deletions

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])