diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index df41951c3..fa7b6791e 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. } *) |