diff options
Diffstat (limited to 'dev/base_include')
| -rw-r--r-- | dev/base_include | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/dev/base_include b/dev/base_include index 66d91f92e1..0f933d6684 100644 --- a/dev/base_include +++ b/dev/base_include @@ -140,6 +140,8 @@ open Hipattern open Inv open Leminv open Refine +open Tacsubst +open Tacintern open Tacinterp open Tacticals open Tactics |