diff options
| author | Pierre-Marie Pédrot | 2020-06-08 19:20:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-19 16:02:25 +0200 |
| commit | c00a369a8bd70efad3e1481daa78ab483038c6cb (patch) | |
| tree | 2609e819b12dc26991df5bad1623c1e486b1c63b /tactics/hints.mli | |
| parent | 9eca7cca68dc82aa738a8d408d75e1b9b5405646 (diff) | |
Move the hint polymorphic status to the hint instance.
It is only used for this kind of hints, never for Extern / Unfold.
Diffstat (limited to 'tactics/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index 29fd90d3ef..8243716624 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -44,6 +44,7 @@ type hint = { hint_type : types; hint_uctx : Univ.ContextSet.t; hint_clnv : clausenv; + hint_poly : bool; } type 'a hints_path_atom_gen = @@ -58,7 +59,6 @@ module FullHint : sig type t val priority : t -> int - val is_polymorphic : t -> bool val pattern : t -> Pattern.constr_pattern option val database : t -> string option val run : t -> (hint hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic |