diff options
| author | Pierre-Marie Pédrot | 2016-06-09 16:50:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-09 17:48:02 +0200 |
| commit | 7527751d9772656b4680df311546825cc2dd3d8f (patch) | |
| tree | 27c07324760d255939dcb9ec556bf8e309ab5186 /tactics | |
| parent | 8efb78da7900e7f13105aac8361272477f8f5119 (diff) | |
Adding a bit of documentation in the mli.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.mli | 4 | ||||
| -rw-r--r-- | tactics/autorewrite.mli | 2 | ||||
| -rw-r--r-- | tactics/class_tactics.mli | 2 | ||||
| -rw-r--r-- | tactics/tactics.mli | 5 |
4 files changed, 10 insertions, 3 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli index 8c4f359041..0fd95aeadb 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This files implements auto and related automation tactics *) + open Names open Term open Clenv @@ -13,8 +15,6 @@ open Pattern open Decl_kinds open Hints -(** Auto and related automation tactics *) - val priority : ('a * full_hint) list -> ('a * full_hint) list val default_search_depth : int ref diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index ac613b57ce..0706571795 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This files implements the autorewrite tactic. *) + open Term open Tacexpr open Equality diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index f1bcfa7dd4..cac4b88445 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This files implements typeclasses eauto *) + open Names open Constr open Tacmach diff --git a/tactics/tactics.mli b/tactics/tactics.mli index df41951c32..fa7b6791ea 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -21,7 +21,10 @@ open Unification open Misctypes open Locus -(** Main tactics. *) +(** Main tactics defined in ML. This file is huge and should probably be split + in more reasonable units at some point. Because of its size and age, the + implementation features various styles and stages of the proof engine. + This has to be uniformized someday. *) (** {6 General functions. } *) |