diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-04-10 15:13:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-04-10 15:13:37 +0200 |
| commit | ba6f6500a948985b091cbf6a05d3631490465081 (patch) | |
| tree | 6cba268852bbedfc3802417d8e57a770b313d012 /tactics/hints.mli | |
| parent | 33650e275a4b3f00541ea87ee4b39892be5fdb2f (diff) | |
Making the hints for the auto tactics private.
They are all generated by the Hints module, and making them purely opaque is
not worthwhile because we project them a lot. This ensures that they all get
generated following a uniform process.
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 45cf562c0..42379b7c0 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -40,7 +40,7 @@ type hints_path_atom = | PathHints of global_reference list | PathAny -type 'a gen_auto_tactic = { +type 'a gen_auto_tactic = private { pri : int; (** A number between 0 and 4, 4 = lower priority *) poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *) pat : constr_pattern option; (** A pattern for the concl of the Goal *) |