From ba6f6500a948985b091cbf6a05d3631490465081 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 10 Apr 2015 15:13:37 +0200 Subject: 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. --- tactics/hints.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/hints.mli') 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 *) -- cgit v1.2.3