Merge PR #13139: Clean the constr-as-hint API

Reviewed-by: SkySkimmer

9 files changed, 50 insertions, 26 deletions

diff --git a/dev/ci/user-overlays/13139-ppedrot-clean-hint-constr.sh b/dev/ci/user-overlays/13139-ppedrot-clean-hint-constr.sh
new file mode 100644
index 0000000000..2f70f43a2b
--- /dev/null
+++ b/dev/ci/user-overlays/13139-ppedrot-clean-hint-constr.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "13139" ] || [ "$CI_BRANCH" = "clean-hint-constr" ]; then
+
+    equations_CI_REF=clean-hint-constr
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+    fiat_parsers_CI_REF=clean-hint-constr
+    fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat
+
+fi
diff --git a/doc/changelog/07-commands-and-options/13139-clean-hint-constr.rst b/doc/changelog/07-commands-and-options/13139-clean-hint-constr.rst
new file mode 100644
index 0000000000..1a6bc88c6c
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/13139-clean-hint-constr.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+  When declaring arbitrary terms as hints, unsolved
+  evars are not abstracted implicitly anymore and instead
+  raise an error
+  (`#13139 <https://github.com/coq/coq/pull/13139>`_,
+  by Pierre-Marie Pédrot).
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index bb2873b486..0c84dee572 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -628,6 +628,9 @@ let subst_var subst c = of_constr (Vars.subst_var subst (to_constr c))
 let subst_univs_level_constr subst c =
   of_constr (Vars.subst_univs_level_constr subst (to_constr c))
 
+let subst_univs_constr subst c =
+  of_constr (UnivSubst.subst_univs_constr subst (to_constr c))
+
 (** Operations that dot NOT commute with evar-normalization *)
 let noccurn sigma n term =
   let rec occur_rec n c = match kind sigma c with
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index a018f4064f..882dfe2848 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -295,6 +295,7 @@ val closedn : Evd.evar_map -> int -> t -> bool
 val closed0 : Evd.evar_map -> t -> bool
 
 val subst_univs_level_constr : Univ.universe_level_subst -> t -> t
+val subst_univs_constr : Univ.universe_subst -> t -> t
 val subst_of_rel_context_instance : rel_context -> t list -> t list
 
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index ed92a85a12..9e66e8668f 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -482,8 +482,7 @@ let make_resolve_hyp env sigma st only_classes pri decl =
   let keep = not only_classes || is_class in
     if keep then
       let id = GlobRef.VarRef id in
-      let name = PathHints [id] in
-        (make_resolves env sigma pri ~name ~check:false (IsGlobRef id))
+      make_resolves env sigma pri id
     else []
 
 let make_hints g (modes,st) only_classes sign =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index fe3efef7c5..68229dbe26 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1347,6 +1347,10 @@ let add_hints ~locality dbnames h =
   | HintsExternEntry (info, tacexp) ->
       add_externs info tacexp ~local ~superglobal dbnames
 
+let hint_globref gr = IsGlobRef gr
+
+let hint_constr (c, diff) = IsConstr (c, diff)
+
 let expand_constructor_hints env sigma lems =
   List.map_append (fun (evd,lem) ->
     match EConstr.kind sigma lem with
@@ -1365,8 +1369,9 @@ let constructor_hints env sigma eapply lems =
   List.map_append (fun lem ->
       make_resolves env sigma (eapply, true) empty_hint_info ~check:true lem) lems
 
-let make_resolves env sigma info ~check ?name hint =
-  make_resolves env sigma (true, false) info ~check ?name hint
+let make_resolves env sigma info hint =
+  let name = PathHints [hint] in
+  make_resolves env sigma (true, false) info ~check:false ~name (IsGlobRef hint)
 
 let make_local_hint_db env sigma ts eapply lems =
   let map c = c env sigma in
diff --git a/tactics/hints.mli b/tactics/hints.mli
index dd22cff10b..3d4d9c7970 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -167,9 +167,7 @@ type hint_db = Hint_db.t
 
 type hnf = bool
 
-type hint_term =
-  | IsGlobRef of GlobRef.t
-  | IsConstr of constr * Univ.ContextSet.t option [@ocaml.deprecated "Declare a hint constant instead"]
+type hint_term
 
 type hints_entry =
   | HintsResolveEntry of (hint_info * hnf * hints_path_atom * hint_term) list
@@ -199,8 +197,10 @@ val current_pure_db : unit -> hint_db list
 
 val add_hints : locality:Goptions.option_locality -> hint_db_name list -> hints_entry -> unit
 
-val prepare_hint : bool (* Check no remaining evars *) ->
-  env -> evar_map -> evar_map * constr -> (constr * Univ.ContextSet.t)
+val hint_globref : GlobRef.t -> hint_term
+
+val hint_constr : constr * Univ.ContextSet.t option -> hint_term
+[@ocaml.deprecated "Declare a hint constant instead"]
 
 (** A constr which is Hint'ed will be:
    - (1) used as an Exact, if it does not start with a product
@@ -210,8 +210,7 @@ val prepare_hint : bool (* Check no remaining evars *) ->
          has missing arguments. *)
 
 val make_resolves :
-  env -> evar_map -> hint_info -> check:bool -> ?name:hints_path_atom ->
-  hint_term -> hint_entry list
+  env -> evar_map -> hint_info -> GlobRef.t -> hint_entry list
 
 (** [make_resolve_hyp hname htyp].
    used to add an hypothesis to the local hint database;
diff --git a/vernac/classes.ml b/vernac/classes.ml
index d5509e2697..a100352145 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -57,7 +57,7 @@ let is_local_for_hint i =
 
 let add_instance_base inst =
   let locality = if is_local_for_hint inst then Goptions.OptLocal else Goptions.OptGlobal in
-  add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] ~locality
+  add_instance_hint (Hints.hint_globref inst.is_impl) [inst.is_impl] ~locality
     inst.is_info
 
 let mk_instance cl info glob impl =
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index 9eac558908..f642411fa4 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -62,7 +62,7 @@ let project_hint ~poly pri l2r r =
       cb
   in
   let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
-  (info, true, Hints.PathAny, Hints.IsGlobRef (GlobRef.ConstRef c))
+  (info, true, Hints.PathAny, Hints.hint_globref (GlobRef.ConstRef c))
 
 let warn_deprecated_hint_constr =
   CWarnings.create ~name:"fragile-hint-constr" ~category:"automation"
@@ -84,16 +84,6 @@ let soft_evaluable =
 let interp_hints ~poly h =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let f poly c =
-    let evd, c = Constrintern.interp_open_constr env sigma c in
-    let env = Global.env () in
-    let sigma = Evd.from_env env in
-    let c, diff = Hints.prepare_hint true env sigma (evd, c) in
-    if poly then (Hints.IsConstr (c, Some diff) [@ocaml.warning "-3"])
-    else
-      let () = DeclareUctx.declare_universe_context ~poly:false diff in
-      (Hints.IsConstr (c, None) [@ocaml.warning "-3"])
-  in
   let fref r =
     let gr = Smartlocate.global_with_alias r in
     Dumpglob.add_glob ?loc:r.CAst.loc gr;
@@ -106,10 +96,22 @@ let interp_hints ~poly h =
     match c with
     | HintsReference c ->
       let gr = Smartlocate.global_with_alias c in
-      (PathHints [gr], IsGlobRef gr)
+      (PathHints [gr], hint_globref gr)
     | HintsConstr c ->
       let () = warn_deprecated_hint_constr () in
-      (PathAny, f poly c)
+      let env = Global.env () in
+      let sigma = Evd.from_env env in
+      let c, uctx = Constrintern.interp_constr env sigma c in
+      let subst, uctx = UState.normalize_variables uctx in
+      let c = EConstr.Vars.subst_univs_constr subst c in
+      let diff = UState.context_set uctx in
+      let c =
+        if poly then (c, Some diff)
+        else
+          let () = DeclareUctx.declare_universe_context ~poly:false diff in
+          (c, None)
+      in
+      (PathAny, Hints.hint_constr c) [@ocaml.warning "-3"]
   in
   let fp = Constrintern.intern_constr_pattern env sigma in
   let fres (info, b, r) =
@@ -149,7 +151,7 @@ let interp_hints ~poly h =
           ( empty_hint_info
           , true
           , PathHints [gr]
-          , IsGlobRef gr ))
+          , hint_globref gr ))
     in
     HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
   | HintsExtern (pri, patcom, tacexp) ->