From ae4346d74acf0d3e48a9660758dd7c064d14f749 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 28 Sep 2020 18:49:30 +0200
Subject: Further API cleanup after the removal of forward hints.

We know statically that only global references are passed to make_resolves.
---
 tactics/class_tactics.ml | 3 +--
 tactics/hints.ml         | 5 +++--
 tactics/hints.mli        | 3 +--
 3 files changed, 5 insertions(+), 6 deletions(-)

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..0170487b2e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1365,8 +1365,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..1bbb506761 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -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;
-- 
cgit v1.2.3


From 511a3eae36d3b57afbbb37b586ef71adf094f8ca Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 2 Oct 2020 18:41:39 +0200
Subject: Encapsulate the last use of IsConstr in the Hints API.

---
 tactics/hints.ml   |  8 ++++++++
 tactics/hints.mli  |  5 +++--
 vernac/comHints.ml | 10 ++++------
 3 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 0170487b2e..b8bd459616 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1347,6 +1347,14 @@ let add_hints ~locality dbnames h =
   | HintsExternEntry (info, tacexp) ->
       add_externs info tacexp ~local ~superglobal dbnames
 
+let hint_constr env sigma ~poly c =
+  let c, diff = prepare_hint true env sigma c in
+  let diff, uctx =
+    if poly then Some diff, Univ.ContextSet.empty
+    else None, diff
+  in
+  IsConstr (c, diff), uctx
+
 let expand_constructor_hints env sigma lems =
   List.map_append (fun (evd,lem) ->
     match EConstr.kind sigma lem with
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 1bbb506761..e74519f12a 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -199,8 +199,9 @@ 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_constr :
+  env -> evar_map -> poly:bool -> evar_map * constr -> hint_term * Univ.ContextSet.t
+  [@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
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index 9eac558908..b5e53208ca 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -85,14 +85,12 @@ 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"])
+    let evd, c = Constrintern.interp_open_constr env sigma c in
+    let h, diff = Hints.hint_constr env sigma ~poly (evd, c) in
+    let () = DeclareUctx.declare_universe_context ~poly:false diff [@ocaml.warning "-3"] in
+    h
   in
   let fref r =
     let gr = Smartlocate.global_with_alias r in
-- 
cgit v1.2.3


From be332604f4d495ea875185ff1b5aee1eb12b4178 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 2 Oct 2020 19:01:46 +0200
Subject: Opacify the Hints.hint_term type.

---
 tactics/hints.ml   |  2 ++
 tactics/hints.mli  |  6 +++---
 vernac/classes.ml  |  2 +-
 vernac/comHints.ml | 21 +++++++++------------
 4 files changed, 15 insertions(+), 16 deletions(-)

diff --git a/tactics/hints.ml b/tactics/hints.ml
index b8bd459616..2bff610b00 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1347,6 +1347,8 @@ 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 env sigma ~poly c =
   let c, diff = prepare_hint true env sigma c in
   let diff, uctx =
diff --git a/tactics/hints.mli b/tactics/hints.mli
index e74519f12a..eb0f937302 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,6 +197,8 @@ val current_pure_db : unit -> hint_db list
 
 val add_hints : locality:Goptions.option_locality -> hint_db_name list -> hints_entry -> unit
 
+val hint_globref : GlobRef.t -> hint_term
+
 val hint_constr :
   env -> evar_map -> poly:bool -> evar_map * constr -> hint_term * Univ.ContextSet.t
   [@ocaml.deprecated "Declare a hint constant instead"]
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 b5e53208ca..6cc1940b40 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,14 +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 env = Global.env () in
-    let sigma = Evd.from_env env in
-    let evd, c = Constrintern.interp_open_constr env sigma c in
-    let h, diff = Hints.hint_constr env sigma ~poly (evd, c) in
-    let () = DeclareUctx.declare_universe_context ~poly:false diff [@ocaml.warning "-3"] in
-    h
-  in
   let fref r =
     let gr = Smartlocate.global_with_alias r in
     Dumpglob.add_glob ?loc:r.CAst.loc gr;
@@ -104,10 +96,15 @@ 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 evd, c = Constrintern.interp_open_constr env sigma c in
+      let h, diff = Hints.hint_constr env sigma ~poly (evd, c) in
+      let () = DeclareUctx.declare_universe_context ~poly:false diff [@ocaml.warning "-3"] in
+      (PathAny, h)
   in
   let fp = Constrintern.intern_constr_pattern env sigma in
   let fres (info, b, r) =
@@ -147,7 +144,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) ->
-- 
cgit v1.2.3


From f4c1b8b9ffdb5e531685130824fc4ce03a3e9794 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 4 Oct 2020 16:16:53 +0200
Subject: Do not try to be clever for term-as-hint interpretation.

The prepare_hint function was trying to requantify over all undefined evars,
but actually this should not happen when defining generic terms as hints through
some Hint vernacular command.
---
 tactics/hints.ml   |  8 +-------
 tactics/hints.mli  |  5 ++---
 vernac/comHints.ml | 18 ++++++++++++++----
 3 files changed, 17 insertions(+), 14 deletions(-)

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 2bff610b00..68229dbe26 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1349,13 +1349,7 @@ let add_hints ~locality dbnames h =
 
 let hint_globref gr = IsGlobRef gr
 
-let hint_constr env sigma ~poly c =
-  let c, diff = prepare_hint true env sigma c in
-  let diff, uctx =
-    if poly then Some diff, Univ.ContextSet.empty
-    else None, diff
-  in
-  IsConstr (c, diff), uctx
+let hint_constr (c, diff) = IsConstr (c, diff)
 
 let expand_constructor_hints env sigma lems =
   List.map_append (fun (evd,lem) ->
diff --git a/tactics/hints.mli b/tactics/hints.mli
index eb0f937302..3d4d9c7970 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -199,9 +199,8 @@ val add_hints : locality:Goptions.option_locality -> hint_db_name list -> hints_
 
 val hint_globref : GlobRef.t -> hint_term
 
-val hint_constr :
-  env -> evar_map -> poly:bool -> evar_map * constr -> hint_term * Univ.ContextSet.t
-  [@ocaml.deprecated "Declare a hint constant instead"]
+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
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index 6cc1940b40..0d32f28d79 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -101,10 +101,20 @@ let interp_hints ~poly h =
       let () = warn_deprecated_hint_constr () in
       let env = Global.env () in
       let sigma = Evd.from_env env in
-      let evd, c = Constrintern.interp_open_constr env sigma c in
-      let h, diff = Hints.hint_constr env sigma ~poly (evd, c) in
-      let () = DeclareUctx.declare_universe_context ~poly:false diff [@ocaml.warning "-3"] in
-      (PathAny, h)
+      let sigma, c = Constrintern.interp_open_constr env sigma c in
+      let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in
+      let sigma, _ = Evd.nf_univ_variables sigma in
+      let c = Evarutil.nf_evar sigma c in
+      let c = Termops.drop_extra_implicit_args sigma c in
+      let () = Pretyping.check_evars env sigma c in
+      let diff = Evd.universe_context_set sigma 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) =
-- 
cgit v1.2.3


From ab6ebfc1f42d96d50763f2dcd6b8322b12613d3d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 6 Oct 2020 14:58:45 +0200
Subject: Further code simplification in arbitrary hint interpretation.

We reuse the standard code path for term interpretation instead of trying
to mangle it.
---
 engine/eConstr.ml  |  3 +++
 engine/eConstr.mli |  1 +
 vernac/comHints.ml | 11 ++++-------
 3 files changed, 8 insertions(+), 7 deletions(-)

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/vernac/comHints.ml b/vernac/comHints.ml
index 0d32f28d79..f642411fa4 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -101,13 +101,10 @@ let interp_hints ~poly h =
       let () = warn_deprecated_hint_constr () in
       let env = Global.env () in
       let sigma = Evd.from_env env in
-      let sigma, c = Constrintern.interp_open_constr env sigma c in
-      let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in
-      let sigma, _ = Evd.nf_univ_variables sigma in
-      let c = Evarutil.nf_evar sigma c in
-      let c = Termops.drop_extra_implicit_args sigma c in
-      let () = Pretyping.check_evars env sigma c in
-      let diff = Evd.universe_context_set sigma 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
-- 
cgit v1.2.3


From be51c8ef5312ab9320421833f6c023ce19459f22 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 14 Oct 2020 11:20:57 +0200
Subject: Document the changes.

---
 doc/changelog/07-commands-and-options/13139-clean-hint-constr.rst | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 doc/changelog/07-commands-and-options/13139-clean-hint-constr.rst

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).
-- 
cgit v1.2.3


From 124135344d6c9ef1f7622b8340c16cc3d5ac8e06 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 5 Oct 2020 16:01:22 +0200
Subject: Add overlays.

---
 dev/ci/user-overlays/13139-ppedrot-clean-hint-constr.sh | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 dev/ci/user-overlays/13139-ppedrot-clean-hint-constr.sh

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
-- 
cgit v1.2.3