Merge branch 'v8.5'

3 files changed, 14 insertions, 8 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index f9b180de6c..6caebf6c4f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -82,11 +82,14 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
       let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
       let map c = Vars.subst_univs_level_constr subst c in
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
-      let clenv = { clenv with evd = evd ; env = Proofview.Goal.env gl } in
-      (** FIXME: We're being inefficient here because we substitute the whole
-          evar map instead of just its metas, which are the only ones
-          mentioning the old universes. *)
-      Clenv.map_clenv map clenv, map c
+      (** Only metas are mentioning the old universes. *)
+      let clenv = {
+        templval = Evd.map_fl map clenv.templval;
+        templtyp = Evd.map_fl map clenv.templtyp;
+        evd = Evd.map_metas map evd;
+        env = Proofview.Goal.env gl;
+      } in
+      clenv, map c
     else
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
       { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 48b9006cd9..97b5ba0cc5 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -71,8 +71,11 @@ let instantiate_tac_by_name id c =
 let let_evar name typ =
   let src = (Loc.ghost,Evar_kinds.GoalEvar) in
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
-    let sigma = Proofview.Goal.sigma gl in
+    let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
+    let sigma = ref sigma in
+    let _ = Typing.sort_of env sigma typ in
+    let sigma = Sigma.Unsafe.of_evar_map !sigma in
     let id = match name with
     | Names.Anonymous -> 
       let id = Namegen.id_of_name_using_hdchar env typ name in
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index d14e7deffd..29002af9e0 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1707,7 +1707,7 @@ let rec strategy_of_ast = function
 let mkappc s l = CAppExpl (Loc.ghost,(None,(Libnames.Ident (Loc.ghost,Id.of_string s)),None),l)
 
 let declare_an_instance n s args =
-  ((Loc.ghost,Name n), Explicit,
+  (((Loc.ghost,Name n),None), Explicit,
   CAppExpl (Loc.ghost, (None, Qualid (Loc.ghost, qualid_of_string s),None),
 	   args))
 
@@ -1923,7 +1923,7 @@ let add_morphism glob binders m s n =
   let poly = Flags.is_universe_polymorphism () in
   let instance_id = add_suffix n "_Proper" in
   let instance =
-    ((Loc.ghost,Name instance_id), Explicit,
+    (((Loc.ghost,Name instance_id),None), Explicit,
     CAppExpl (Loc.ghost,
 	     (None, Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
 	     [cHole; s; m]))