diff options
| author | Pierre-Marie Pédrot | 2020-10-04 16:16:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-04 13:43:57 +0100 |
| commit | f4c1b8b9ffdb5e531685130824fc4ce03a3e9794 (patch) | |
| tree | b68dcc1bd537c1108d2aa92642bca3b2725c9333 /tactics | |
| parent | be332604f4d495ea875185ff1b5aee1eb12b4178 (diff) | |
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.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hints.ml | 8 | ||||
| -rw-r--r-- | tactics/hints.mli | 5 |
2 files changed, 3 insertions, 10 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 |