diff options
| author | Hugo Herbelin | 2014-10-07 17:26:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-07 18:40:36 +0200 |
| commit | 38b34dfffcceab7fa7d5ba43c84e414d24cebe43 (patch) | |
| tree | c5449cf9c02c97586bf8a8edaa52d05d876d3e94 /tactics/tactics.mllib | |
| parent | 2313bde0116a5916912bebbaca77d291f7b2760a (diff) | |
Splitting out of auto.ml a file hints.ml dedicated to hints so as to
being able to export hints without tactics, vm, etc. to come with.
Some functions moved to the new proof engine.
Diffstat (limited to 'tactics/tactics.mllib')
| -rw-r--r-- | tactics/tactics.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index e2c0f40fb9..46f2abd7f5 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -17,6 +17,7 @@ Leminv Tacsubst Taccoerce Tacenv +Hints Auto Tacintern TacticMatching |