Merge branch 'v8.5'

6 files changed, 41 insertions, 26 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 2b3fadf7fa..3a9d40de03 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -292,10 +292,13 @@ let find_applied_relation metas loc env sigma c left2right =
 (* To add rewriting rules to a base *)
 let add_rew_rules base lrul =
   let counter = ref 0 in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
   let lrul =
     List.fold_left
       (fun dn (loc,(c,ctx),b,t) ->
-	let info = find_applied_relation false loc (Global.env ()) Evd.empty c b in
+	let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
+	let info = find_applied_relation false loc env sigma c b in
 	let pat = if b then info.hyp_left else info.hyp_right in
 	let rul = { rew_lemma = c; rew_type = info.hyp_ty;
 		    rew_pat = pat; rew_ctx = ctx; rew_l2r = b;
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a10d8a0747..4c48003b93 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -335,7 +335,9 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
   | Ind (ind,u) -> 
       let c, eff = find_scheme scheme_name ind in 
       (* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *)
-      let sigma, elim = Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
+      let sigma, elim =
+	Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c)
+      in
 	sigma, elim, eff
   | _ -> assert false
 
@@ -899,7 +901,7 @@ let discrimination_pf env sigma e (t,t1,t2) discriminator lbeq =
   let i            = build_coq_I () in
   let absurd_term  = build_coq_False () in
   let eq_elim, eff = ind_scheme_of_eq lbeq in
-  let sigma, eq_elim = Evd.fresh_global env sigma eq_elim in
+  let sigma, eq_elim = Evd.fresh_global (Global.env ()) sigma eq_elim in
     sigma, (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term),
     eff
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index af0870bc92..cab74968d2 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -262,16 +262,15 @@ TACTIC EXTEND rewrite_star
 (* Hint Rewrite                                                       *)
 
 let add_rewrite_hint bases ort t lcsr =
-  let env = Global.env() and sigma = Evd.empty in
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
   let poly = Flags.is_universe_polymorphism () in 
   let f ce = 
     let c, ctx = Constrintern.interp_constr env sigma ce in
     let ctx =
-      if poly then 
-	Evd.evar_universe_context_set Univ.UContext.empty ctx
-      else 
-	let cstrs = Evd.evar_universe_context_constraints ctx in
-	  (Global.add_constraints cstrs; Univ.ContextSet.empty)
+      let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in
+        if poly then ctx
+	else (Global.push_context_set false ctx; Univ.ContextSet.empty)
     in
       Constrexpr_ops.constr_loc ce, (c, ctx), ort, t in
   let eqs = List.map f lcsr in
@@ -490,7 +489,9 @@ let inTransitivity : bool * constr -> obj =
 (* Main entry points *)
 
 let add_transitivity_lemma left lem =
- let lem',ctx (*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty lem in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let lem',ctx (*FIXME*) = Constrintern.interp_constr env sigma lem in
   add_anonymous_leaf (inTransitivity (left,lem'))
 
 (* Vernacular syntax *)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 0df1a35c62..a7eae667d0 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1085,8 +1085,10 @@ let prepare_hint check env init (sigma,c) =
 
 let interp_hints poly =
   fun h ->
+  let env = (Global.env()) in
+  let sigma = Evd.from_env env in
   let f c =
-    let evd,c = Constrintern.interp_open_constr (Global.env()) Evd.empty c in
+    let evd,c = Constrintern.interp_open_constr env sigma c in
       prepare_hint true (Global.env()) Evd.empty (evd,c) in
   let fref r =
     let gr = global_with_alias r in
@@ -1135,7 +1137,8 @@ let add_hints local dbnames0 h =
   if String.List.mem "nocore" dbnames0 then
     error "The hint database \"nocore\" is meant to stay empty.";
   let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in
-  let env = Global.env() and sigma = Evd.empty in
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
   match h with
   | HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames
   | HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index c64a1226ab..937ad2b9d4 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1797,11 +1797,13 @@ let proper_projection r ty =
     it_mkLambda_or_LetIn app ctx
 
 let declare_projection n instance_id r =
-  let c,uctx = Universes.fresh_global_instance (Global.env()) r in
   let poly = Global.is_polymorphic r in
-  let ty = Retyping.get_type_of (Global.env ()) Evd.empty c in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let evd,c = Evd.fresh_global env sigma r in
+  let ty = Retyping.get_type_of env sigma c in
   let term = proper_projection c ty in
-  let typ = Typing.unsafe_type_of (Global.env ()) Evd.empty term in
+  let typ = Typing.unsafe_type_of env sigma term in
   let ctx, typ = decompose_prod_assum typ in
   let typ =
     let n =
@@ -1824,15 +1826,16 @@ let declare_projection n instance_id r =
   in
   let typ = it_mkProd_or_LetIn typ ctx in
   let cst = 
-    Declare.definition_entry ~types:typ ~poly ~univs:(Univ.ContextSet.to_context uctx) 
-      term 
+    Declare.definition_entry ~types:typ ~poly
+      ~univs:(Evd.universe_context sigma) term
   in
     ignore(Declare.declare_constant n 
 	   (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
 
 let build_morphism_signature m =
   let env = Global.env () in
-  let m,ctx = Constrintern.interp_constr env (Evd.from_env env) m in
+  let sigma = Evd.from_env env in
+  let m,ctx = Constrintern.interp_constr env sigma m in
   let sigma = Evd.from_ctx ctx in
   let t = Typing.unsafe_type_of env sigma m in
   let cstrs =
@@ -1844,7 +1847,7 @@ let build_morphism_signature m =
     in aux t
   in
   let evars, t', sig_, cstrs = 
-    PropGlobal.build_signature (Evd.empty, Evar.Set.empty) env t cstrs None in
+    PropGlobal.build_signature (sigma, Evar.Set.empty) env t cstrs None in
   let evd = ref evars in
   let _ = List.iter
     (fun (ty, rel) ->
@@ -1861,9 +1864,10 @@ let build_morphism_signature m =
 
 let default_morphism sign m =
   let env = Global.env () in
-  let t = Typing.unsafe_type_of env Evd.empty m in
+  let sigma = Evd.from_env env in
+  let t = Typing.unsafe_type_of env sigma m in
   let evars, _, sign, cstrs =
-    PropGlobal.build_signature (Evd.empty, Evar.Set.empty) env t (fst sign) (snd sign)
+    PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign)
   in
   let evars, morph = app_poly_check env evars PropGlobal.proper_type [| t; sign; m |] in
   let evars, mor = resolve_one_typeclass env (goalevars evars) morph in
@@ -1894,7 +1898,7 @@ let add_morphism_infer glob m n =
   let poly = Flags.is_universe_polymorphism () in
   let instance_id = add_suffix n "_Proper" in
   let instance = build_morphism_signature m in
-  let evd = Evd.empty (*FIXME *) in
+  let evd = Evd.from_env (Global.env ()) in
     if Lib.is_modtype () then
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
 				(Entries.ParameterEntry 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 7d1cc3341c..bc82e9ef46 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -593,10 +593,12 @@ module New = struct
   (* c should be of type A1->.. An->B with B an inductive definition *)
   let general_elim_then_using mk_elim
       isrec allnames tac predicate ind (c, t) =
-    Proofview.Goal.nf_enter begin fun gl ->
-    let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in
-    (** FIXME: evar leak. *)
+    Proofview.Goal.nf_enter
+    begin fun gl ->
     let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+    (Proofview.Goal.nf_enter begin fun gl ->
+    let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in
     (* applying elimination_scheme just a little modified *)
     let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in
     let indmv =
@@ -647,7 +649,7 @@ module New = struct
     Proofview.tclTHEN
       (Clenvtac.clenv_refine false clenv')
       (Proofview.tclEXTEND [] tclIDTAC branchtacs)
-    end
+    end) end
 
   let elimination_then tac c =
     Proofview.Goal.nf_enter begin fun gl ->