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

11 files changed, 57 insertions, 47 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index a4eae5fdff..128a7e55c4 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -355,47 +355,41 @@ let new_pure_evar_full evd evi =
   let evd = Evd.add evd evk evi in
   (evd, evk)
 
-let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates typ =
+let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates ?store typ =
   let newevk = new_untyped_evar() in
-  let evd = evar_declare sign newevk typ ~src ?filter ?candidates evd in
+  let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store evd in
   (evd,newevk)
 
-let new_evar_instance sign evd typ ?src ?filter ?candidates instance =
+let new_evar_instance sign evd typ ?src ?filter ?candidates ?store instance =
   assert (not !Flags.debug ||
             List.distinct (ids_of_named_context (named_context_of_val sign)));
-  let evd,newevk = new_pure_evar evd sign ?src ?filter ?candidates typ in
+  let evd,newevk = new_pure_evar evd sign ?src ?filter ?candidates ?store typ in
   (evd,mkEvar (newevk,Array.of_list instance))
 
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
-let new_evar evd env ?src ?filter ?candidates typ =
+let new_evar evd env ?src ?filter ?candidates ?store typ =
   let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in
   let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in
   let instance =
     match filter with
     | None -> instance
     | Some filter -> Filter.filter_list filter instance in
-  new_evar_instance sign evd typ' ?src ?filter ?candidates instance
+  new_evar_instance sign evd typ' ?src ?filter ?candidates ?store instance
 
 let new_type_evar ?src ?filter rigid evd env =
   let evd', s = new_sort_variable rigid evd in
   let evd', e = new_evar evd' env ?src ?filter (mkSort s) in
     evd', (e, s)
 
-  (* The same using side-effect *)
-let e_new_evar evdref env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?filter ?candidates ty =
-  let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ty in
-  evdref := evd';
-  ev
-
 let e_new_type_evar evdref ?src ?filter rigid env =
   let evd', c = new_type_evar ?src ?filter rigid !evdref env in
     evdref := evd';
     c
 
   (* The same using side-effect *)
-let e_new_evar evdref env ?(src=default_source) ?filter ?candidates ty =
-  let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ty in
+let e_new_evar evdref env ?(src=default_source) ?filter ?candidates ?store ty =
+  let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ?store ty in
   evdref := evd';
   ev
 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index d197ad2efe..7715691b0c 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -23,18 +23,18 @@ val mk_new_meta : unit -> constr
 (** {6 Creating a fresh evar given their type and context} *)
 val new_evar :
   evar_map -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?candidates:constr list -> types -> evar_map * constr
+  ?candidates:constr list -> ?store:Store.t -> types -> evar_map * constr
 
 val new_pure_evar :
   evar_map -> named_context_val -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?candidates:constr list -> types -> evar_map * evar
+  ?candidates:constr list -> ?store:Store.t -> types -> evar_map * evar
 
 val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar
 
 (** the same with side-effects *)
 val e_new_evar :
   evar_map ref -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?candidates:constr list -> types -> constr
+  ?candidates:constr list -> ?store:Store.t -> types -> constr
 
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
@@ -57,7 +57,9 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr
    of [inst] are typed in the occurrence context and their type (seen
    as a telescope) is [sign] *)
 val new_evar_instance :
- named_context_val -> evar_map -> types -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> constr list -> evar_map * constr
+ named_context_val -> evar_map -> types -> 
+  ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> 
+  ?store:Store.t -> constr list -> evar_map * constr
 
 val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 1bd995d5d1..5a9281c890 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -295,7 +295,6 @@ let is_empty_evar_universe_context ctx =
 
 let union_evar_universe_context ctx ctx' =
   if ctx == ctx' then ctx
-  else if is_empty_evar_universe_context ctx then ctx'
   else if is_empty_evar_universe_context ctx' then ctx
   else
     let local = 
@@ -331,7 +330,7 @@ let diff_evar_universe_context ctx' ctx  =
 	  Univ.LSet.diff ctx'.uctx_univ_algebraic ctx.uctx_univ_algebraic;
 	uctx_univ_template = 
 	  Univ.LSet.diff ctx'.uctx_univ_template ctx.uctx_univ_template;
-	uctx_universes = Univ.empty_universes;
+	uctx_universes = ctx.uctx_initial_universes;
 	uctx_initial_universes = ctx.uctx_initial_universes }
 
 (* let diff_evar_universe_context_key = Profile.declare_profile "diff_evar_universe_context";; *)
@@ -354,7 +353,7 @@ let instantiate_variable l b v =
 
 exception UniversesDiffer
 
-let process_universe_constraints univs vars alg templ local cstrs =
+let process_universe_constraints univs vars alg templ cstrs =
   let vars = ref vars in
   let normalize = Universes.normalize_universe_opt_subst vars in
   let rec unify_universes fo l d r local =
@@ -370,10 +369,11 @@ let process_universe_constraints univs vars alg templ local cstrs =
 	    if Univ.check_leq univs l r then
 	      (** Keep Prop/Set <= var around if var might be instantiated by prop or set
 		  later. *)
-	      if Univ.is_small_univ l && not (Univ.is_small_univ r) then
-		match Univ.Universe.level l, Univ.Universe.level r with
-		| Some l, Some r -> Univ.Constraint.add (l,Univ.Le,r) local
-		| _, _ -> local
+	      if Univ.is_small_univ l then 
+		match Univ.Universe.level r with
+		| Some r when Univ.LMap.mem r !vars -> 
+		  Univ.Constraint.add (Option.get (Univ.Universe.level l),Univ.Le,r) local
+		| _ -> local
 	      else local
 	    else
 	      match Univ.Universe.level r with
@@ -423,7 +423,7 @@ let process_universe_constraints univs vars alg templ local cstrs =
   in
   let local = 
     Univ.UniverseConstraints.fold (fun (l,d,r) local -> unify_universes false l d r local)
-      cstrs local
+      cstrs Univ.Constraint.empty
   in
     !vars, local
 
@@ -440,7 +440,7 @@ let add_constraints_context ctx cstrs =
   let vars, local' =
     process_universe_constraints ctx.uctx_universes
       ctx.uctx_univ_variables ctx.uctx_univ_algebraic
-      ctx.uctx_univ_template local cstrs'
+      ctx.uctx_univ_template cstrs'
   in
     { ctx with uctx_local = (univs, Univ.Constraint.union local local');
       uctx_univ_variables = vars;
@@ -454,7 +454,7 @@ let add_universe_constraints_context ctx cstrs =
   let vars, local' = 
     process_universe_constraints ctx.uctx_universes 
       ctx.uctx_univ_variables ctx.uctx_univ_algebraic 
-      ctx.uctx_univ_template local cstrs 
+      ctx.uctx_univ_template cstrs 
   in
     { ctx with uctx_local = (univs, Univ.Constraint.union local local');
       uctx_univ_variables = vars;
@@ -769,7 +769,8 @@ let define evk body evd =
   in
   { evd with defn_evars; undf_evars; last_mods; }
 
-let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?(filter = Filter.identity) ?candidates evd =
+let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) 
+    ?(filter=Filter.identity) ?candidates ?(store=Store.empty) evd =
   let () = match Filter.repr filter with
   | None -> ()
   | Some filter ->
@@ -782,7 +783,7 @@ let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?(filter
     evar_filter = filter;
     evar_source = src;
     evar_candidates = candidates;
-    evar_extra = Store.empty; }
+    evar_extra = store; }
   in
   { evd with undf_evars = EvMap.add evk evar_info evd.undf_evars; }
 
@@ -1128,9 +1129,9 @@ let set_leq_sort evd s1 s2 =
       | Prop c, Prop c' -> 
 	  if c == Null && c' == Pos then evd
 	  else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])))
-      | _, _ ->
+      | _, _ -> 
         add_universe_constraints evd (Univ.UniverseConstraints.singleton (u1,Univ.ULe,u2))
-	
+	    
 let check_eq evd s s' =
   Univ.check_eq evd.universes.uctx_universes s s'
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index fb348ae226..49a91f524e 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -234,7 +234,8 @@ val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool ->
 
 val evar_declare :
   named_context_val -> evar -> types -> ?src:Loc.t * Evar_kinds.t ->
-      ?filter:Filter.t -> ?candidates:constr list -> evar_map -> evar_map
+      ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> 
+  evar_map -> evar_map
 (** Convenience function. Just a wrapper around {!add}. *)
 
 val evar_source : existential_key -> evar_map -> Evar_kinds.t located
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index ada497ece7..8364387783 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -507,6 +507,9 @@ let is_implicit_arg = function
 
 let resolvable = Store.field ()
 
+let set_resolvable s b =
+  Store.set s resolvable b
+
 let is_resolvable evi =
   assert (match evi.evar_body with Evar_empty -> true | _ -> false);
   Option.default true (Store.get evi.evar_extra resolvable)
@@ -540,7 +543,7 @@ let mark_resolvability filter b sigma =
   Evd.raw_map_undefined map sigma
 
 let mark_unresolvables ?(filter=all_evars) sigma = mark_resolvability filter false sigma
-let mark_resolvables sigma = mark_resolvability all_evars true sigma
+let mark_resolvables ?(filter=all_evars) sigma = mark_resolvability filter true sigma
 
 let has_typeclasses filter evd =
   let check ev evi =
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index a8ce9ca7c9..ebc6be45fb 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -92,11 +92,12 @@ val no_goals_or_obligations : evar_filter
 (** Resolvability.
     Only undefined evars can be marked or checked for resolvability. *)
 
+val set_resolvable : Evd.Store.t -> bool -> Evd.Store.t
 val is_resolvable : evar_info -> bool
 val mark_unresolvable : evar_info -> evar_info
 val mark_unresolvables : ?filter:evar_filter -> evar_map -> evar_map
+val mark_resolvables   : ?filter:evar_filter -> evar_map -> evar_map
 val mark_resolvable : evar_info -> evar_info
-val mark_resolvables : evar_map -> evar_map
 val is_class_evar : evar_map -> evar_info -> bool
 
 val resolve_typeclasses : ?filter:evar_filter -> ?split:bool -> ?fail:bool ->
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index e49a57af39..5cb677d1c6 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -226,7 +226,7 @@ let start_proof id str goals terminator =
   let initial_state = {
     pid = id;
     terminator = Ephemeron.create terminator;
-    proof = Proof.start Evd.empty goals;
+    proof = Proof.start (Evd.from_env (Global.env ())) goals;
     endline_tactic = None;
     section_vars = None;
     strength = str;
@@ -237,7 +237,7 @@ let start_dependent_proof id str goals terminator =
   let initial_state = {
     pid = id;
     terminator = Ephemeron.create terminator;
-    proof = Proof.dependent_start Evd.empty goals;
+    proof = Proof.dependent_start (Evd.from_env (Global.env ())) goals;
     endline_tactic = None;
     section_vars = None;
     strength = str;
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])
diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v
index d7e598fb4e..e4e1fe3b03 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 *)
 
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index a0ee4caaa5..ac52d1bbb9 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -110,7 +110,7 @@ Proof.
  intros x x' Hx y y' Hy.
  assert (H1 := max_spec x y). assert (H2 := max_spec x' y').
  set (m := max x y) in *; set (m' := max x' y') in *; clearbody m m'.
- rewrite <- Hx, <- Hy in *.
+ rewrite <- Hx, <- Hy in *. 
  destruct (lt_total x y); intuition order.
 Qed.
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index f4171da1b3..bc6f88e691 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -245,7 +245,7 @@ let declare_assumptions idl is_coe k c imps impl_is_on nl =
 
 let do_assumptions kind nl l =
   let env = Global.env () in
-  let evdref = ref Evd.empty in
+  let evdref = ref (Evd.from_env env) in
   let _,l = List.fold_map (fun env (is_coe,(idl,c)) ->
     let (t,ctx),imps = interp_assumption evdref env [] c in
     let env =
@@ -752,8 +752,8 @@ let nf_evar_context sigma ctx =
 
 let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
-  let evdref = ref Evd.empty in
   let env = Global.env() in
+  let evdref = ref (Evd.from_env env) in
   let _, ((env', binders_rel), impls) = interp_context_evars evdref env bl in
   let len = List.length binders_rel in
   let top_env = push_rel_context binders_rel env in
@@ -892,7 +892,7 @@ let interp_recursive isfix fixl notations =
   let fixnames = List.map (fun fix -> fix.fix_name) fixl in
 
   (* Interp arities allowing for unresolved types *)
-  let evdref = ref Evd.empty in
+  let evdref = ref (Evd.from_env env) in
   let fixctxs, fiximppairs, fixannots =
     List.split3 (List.map (interp_fix_context evdref env isfix) fixl) in
   let fixctximpenvs, fixctximps = List.split fiximppairs in
@@ -978,8 +978,10 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe
     let env = Global.env() in
     let indexes = search_guard Loc.ghost env indexes fixdecls in
     let fiximps = List.map (fun (n,r,p) -> r) fiximps in
+    let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
     let fixdecls =
       List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
+    let ctx = Universes.restrict_universe_context ctx vars in
     let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
     let ctx = Univ.ContextSet.to_context ctx in
     ignore (List.map4 (declare_fix (local, poly, Fixpoint) ctx)