Merge branch 'v8.5'

10 files changed, 58 insertions, 34 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index e5fdf6a7c2..617c491c35 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -72,27 +72,42 @@ let auto_flags_of_state st =
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
-let unify_resolve_nodelta poly (c,clenv) =
+let unify_resolve poly flags ((c : raw_hint), clenv) =
   Proofview.Goal.nf_enter begin fun gl ->
-  let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
-  let clenv' = Tacmach.New.of_old connect_clenv gl clenv' in
-  let clenv'' = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags:auto_unif_flags clenv' gl) gl in
-  Clenvtac.clenv_refine false clenv''
+  (** [clenv] has been generated by a hint-making function, so the only relevant
+      data in its evarmap is the set of metas. The [evar_reset_evd] function
+      below just replaces the metas of sigma by those coming from the clenv. *)
+  let sigma = Proofview.Goal.sigma gl in
+  let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
+  (** Still, we need to update the universes *)
+  let (_, _, ctx) = c in
+  let clenv =
+    if poly then
+      (** Refresh the instance of the hint *)
+      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
+    else
+      let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
+      { clenv with evd = evd ; env = Proofview.Goal.env gl }
+  in
+  let clenv = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv gl) gl in
+  Clenvtac.clenv_refine false clenv
   end
 
-let unify_resolve poly flags (c,clenv) =
-  Proofview.Goal.nf_enter begin fun gl ->
-  let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
-  let clenv' = Tacmach.New.of_old connect_clenv gl clenv' in
-  let clenv'' = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv' gl) gl in
-  Clenvtac.clenv_refine false clenv''
-  end
+let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h
 
 let unify_resolve_gen poly = function
   | None -> unify_resolve_nodelta poly
   | Some flags -> unify_resolve poly flags
 
 let exact poly (c,clenv) =
+  let (c, _, _) = c in
   let ctx, c' = 
     if poly then
       let evd', subst = Evd.refresh_undefined_universes clenv.evd in
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 8dacc13629..6e2acf7f56 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -26,9 +26,9 @@ val default_search_depth : int ref
 val auto_flags_of_state : transparent_state -> Unification.unify_flags
 
 (** Try unification with the precompiled clause, then use registered Apply *)
-val unify_resolve_nodelta : polymorphic -> (constr * clausenv) -> unit Proofview.tactic
+val unify_resolve_nodelta : polymorphic -> (raw_hint * clausenv) -> unit Proofview.tactic
 
-val unify_resolve : polymorphic -> Unification.unify_flags -> (constr * clausenv) -> unit Proofview.tactic
+val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic
 
 (** [ConclPattern concl pat tacast]:
    if the term concl matches the pattern pat, (in sense of
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index ca0a74fee1..c30957a673 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -154,6 +154,7 @@ let progress_evars t =
 
 
 let e_give_exact flags poly (c,clenv) gl =
+  let (c, _, _) = c in
   let c, gl =
     if poly then
       let clenv', subst = Clenv.refresh_undefined_univs clenv in
@@ -179,6 +180,7 @@ let unify_resolve poly flags (c,clenv) gls =
     (Clenvtac.clenv_refine false ~with_classes:false clenv') gls
 
 let clenv_of_prods poly nprods (c, clenv) gls =
+  let (c, _, _) = c in
   if poly || Int.equal nprods 0 then Some clenv
   else
     let ty = pf_unsafe_type_of gls c in
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index f39d714628..1a84161e40 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -126,6 +126,7 @@ open Unification
 let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
 
 let unify_e_resolve poly flags (c,clenv) gls =
+  let (c, _, _) = c in
   let clenv', subst = if poly then Clenv.refresh_undefined_univs clenv 
   else clenv, Univ.empty_level_subst in
   let clenv' = connect_clenv gls clenv' in
@@ -142,6 +143,7 @@ let hintmap_of hdc concl =
    (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
 
 let e_exact poly flags (c,clenv) =
+  let (c, _, _) = c in
   let clenv', subst = 
     if poly then Clenv.refresh_undefined_univs clenv 
     else clenv, Univ.empty_level_subst
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 4c48003b93..a74d555dd0 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -88,7 +88,7 @@ type freeze_evars_flag = bool (* true = don't instantiate existing evars *)
 type orientation = bool
 
 type conditions =
-  | Naive (* Only try the first occurence of the lemma (default) *)
+  | Naive (* Only try the first occurrence of the lemma (default) *)
   | FirstSolved (* Use the first match whose side-conditions are solved *)
   | AllMatches (* Rewrite all matches whose side-conditions are solved *)
 
@@ -1577,7 +1577,7 @@ let restrict_to_eq_and_identity eq = (* compatibility *)
 
 exception FoundHyp of (Id.t * constr * bool)
 
-(* tests whether hyp [c] is [x = t] or [t = x], [x] not occuring in [t] *)
+(* tests whether hyp [c] is [x = t] or [t = x], [x] not occurring in [t] *)
 let is_eq_x gl x (id,_,c) =
   try
     let c = pf_nf_evar gl c in
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 3e13ee570c..840ede7d9f 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -23,7 +23,7 @@ type freeze_evars_flag = bool (* true = don't instantiate existing evars *)
 type orientation = bool
 
 type conditions =
-  | Naive (* Only try the first occurence of the lemma (default) *)
+  | Naive (* Only try the first occurrence of the lemma (default) *)
   | FirstSolved (* Use the first match whose side-conditions are solved *)
   | AllMatches (* Rewrite all matches whose side-conditions are solved *)
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 9faa96a806..96c7d79ca5 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -97,7 +97,9 @@ type 'a with_uid = {
   uid : KerName.t;
 }
 
-type hint = (constr * clausenv) hint_ast with_uid
+type raw_hint = constr * types * Univ.universe_context_set
+
+type hint = (raw_hint * clausenv) hint_ast with_uid
 
 type 'a with_metadata = {
   pri  : int;            (* A number lower is higher priority *)
@@ -110,7 +112,7 @@ type 'a with_metadata = {
 type full_hint = hint with_metadata
 
 type hint_entry = global_reference option * 
-  (constr * types * Univ.universe_context_set) hint_ast with_uid with_metadata
+  raw_hint hint_ast with_uid with_metadata
 
 type import_level = [ `LAX | `WARN | `STRICT ]
 
@@ -267,7 +269,7 @@ let strip_params env c =
   | _ -> c
 
 let instantiate_hint env sigma p =
-  let mk_clenv c cty ctx =
+  let mk_clenv (c, cty, ctx) =
     let sigma = Evd.merge_context_set univ_flexible sigma ctx in
     let cl = mk_clenv_from_env env sigma None (c,cty) in 
       {cl with templval = 
@@ -275,11 +277,11 @@ let instantiate_hint env sigma p =
 	env = empty_env}
   in
   let code = match p.code.obj with
-    | Res_pf (c, cty, ctx) -> Res_pf (c, mk_clenv c cty ctx)
-    | ERes_pf (c, cty, ctx) -> ERes_pf (c, mk_clenv c cty ctx)
-    | Res_pf_THEN_trivial_fail (c, cty, ctx) ->
-      Res_pf_THEN_trivial_fail (c, mk_clenv c cty ctx)
-    | Give_exact (c, cty, ctx) -> Give_exact (c, mk_clenv c cty ctx)
+    | Res_pf c -> Res_pf (c, mk_clenv c)
+    | ERes_pf c -> ERes_pf (c, mk_clenv c)
+    | Res_pf_THEN_trivial_fail c ->
+      Res_pf_THEN_trivial_fail (c, mk_clenv c)
+    | Give_exact c -> Give_exact (c, mk_clenv c)
     | Unfold_nth e -> Unfold_nth e
     | Extern t -> Extern t
   in
@@ -1205,12 +1207,14 @@ let make_db_list dbnames =
 (*                    Functions for printing the hints                    *)
 (**************************************************************************)
 
+let pr_hint_elt (c, _, _) = pr_constr c
+
 let pr_hint h = match h.obj with
-  | Res_pf (c,clenv) -> (str"apply " ++ pr_constr c)
-  | ERes_pf (c,clenv) -> (str"eapply " ++ pr_constr c)
-  | Give_exact (c,clenv) -> (str"exact " ++ pr_constr c)
-  | Res_pf_THEN_trivial_fail (c,clenv) ->
-      (str"apply " ++ pr_constr c ++ str" ; trivial")
+  | Res_pf (c, _) -> (str"apply " ++ pr_hint_elt c)
+  | ERes_pf (c, _) -> (str"eapply " ++ pr_hint_elt c)
+  | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt c)
+  | Res_pf_THEN_trivial_fail (c, _) ->
+      (str"apply " ++ pr_hint_elt c ++ str" ; trivial")
   | Unfold_nth c -> (str"unfold " ++  pr_evaluable_reference c)
   | Extern tac ->
       let env =
diff --git a/tactics/hints.mli b/tactics/hints.mli
index e25b66b27b..af4d3d1f66 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -37,6 +37,7 @@ type 'a hint_ast =
   | Extern     of Tacexpr.glob_tactic_expr       (* Hint Extern *)
 
 type hint
+type raw_hint = constr * types * Univ.universe_context_set
 
 type hints_path_atom = 
   | PathHints of global_reference list
@@ -199,11 +200,11 @@ val make_extern :
       -> hint_entry
 
 val run_hint : hint ->
-  ((constr * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
+  ((raw_hint * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
 
 (** This function is for backward compatibility only, not to use in newly
     written code. *)
-val repr_hint : hint -> (constr * clausenv) hint_ast
+val repr_hint : hint -> (raw_hint * clausenv) hint_ast
 
 val extern_intern_tac :
   (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index efd6ded44c..42d22bc3c4 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -124,7 +124,7 @@ let rec add_prods_sign env sigma t =
         add_prods_sign (push_named (id,Some c1,t1) env) sigma b'
     | _ -> (env,t)
 
-(* [dep_option] indicates wether the inversion lemma is dependent or not.
+(* [dep_option] indicates whether the inversion lemma is dependent or not.
    If it is dependent and I is of the form (x_bar:T_bar)(I t_bar) then
    the stated goal will be (x_bar:T_bar)(H:(I t_bar))(P t_bar H)
    where P:(x_bar:T_bar)(H:(I x_bar))[sort].
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 6bd65d0a21..0811708695 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1386,7 +1386,7 @@ module Strategies =
 
 end
 
-(** The strategy for a single rewrite, dealing with occurences. *)
+(** The strategy for a single rewrite, dealing with occurrences. *)
 
 (** A dummy initial clauseenv to avoid generating initial evars before
     even finding a first application of the rewriting lemma, in setoid_rewrite