diff options
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 |