From 674dcda367d9ed43f3b0cc8264a0ef10bc7fd751 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 3 Sep 2020 14:28:05 +0200
Subject: Statically ensure that only polymophic hint terms come with a
 context.

It is the duty of the caller to properly declare monomorphic global
constraints when creating a non-globref hint. All callers were already
abiding by this convention.
---
 tactics/hints.mli | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'tactics/hints.mli')

diff --git a/tactics/hints.mli b/tactics/hints.mli
index e061bd7648..dd22cff10b 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -42,9 +42,8 @@ type 'a hint_ast =
 type hint = private {
   hint_term : constr;
   hint_type : types;
-  hint_uctx : Univ.ContextSet.t;
+  hint_uctx : Univ.ContextSet.t option;
   hint_clnv : clausenv;
-  hint_poly : bool;
 }
 
 type 'a hints_path_atom_gen =
@@ -170,11 +169,11 @@ type hnf = bool
 
 type hint_term =
   | IsGlobRef of GlobRef.t
-  | IsConstr of constr * Univ.ContextSet.t [@ocaml.deprecated "Declare a hint constant instead"]
+  | IsConstr of constr * Univ.ContextSet.t option [@ocaml.deprecated "Declare a hint constant instead"]
 
 type hints_entry =
-  | HintsResolveEntry of (hint_info * bool * hnf * hints_path_atom * hint_term) list
-  | HintsImmediateEntry of (hints_path_atom * bool * hint_term) list
+  | HintsResolveEntry of (hint_info * hnf * hints_path_atom * hint_term) list
+  | HintsImmediateEntry of (hints_path_atom * hint_term) list
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool
@@ -211,7 +210,7 @@ val prepare_hint : bool (* Check no remaining evars *) ->
          has missing arguments. *)
 
 val make_resolves :
-  env -> evar_map -> hint_info -> check:bool -> poly:bool -> ?name:hints_path_atom ->
+  env -> evar_map -> hint_info -> check:bool -> ?name:hints_path_atom ->
   hint_term -> hint_entry list
 
 (** [make_resolve_hyp hname htyp].
-- 
cgit v1.2.3