diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 01:23:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 02:21:42 +0100 |
| commit | 9f5d9cd2622f3890e70dad01898868fe29df6048 (patch) | |
| tree | 82b24258f3cc39e2c64defb112094faafeeb2774 /tactics/hightactics.mllib | |
| parent | 01cd0dd64e4faa52b5094a99e2c31ecc4e7b767d (diff) | |
Moving the tactic related code from Metasyntax to a new file.
Diffstat (limited to 'tactics/hightactics.mllib')
| -rw-r--r-- | tactics/hightactics.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib index 0649f2f72..b18d148ec 100644 --- a/tactics/hightactics.mllib +++ b/tactics/hightactics.mllib @@ -1,3 +1,4 @@ +Tacentries Tacinterp Evar_tactics Tactic_option |