diff options
Diffstat (limited to 'dev/base_include')
| -rw-r--r-- | dev/base_include | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/dev/base_include b/dev/base_include index b6c2e4d08f..41d1ac3bbc 100644 --- a/dev/base_include +++ b/dev/base_include @@ -53,6 +53,7 @@ open Names open Term open Typeops +open Term_typing open Univ open Inductive open Indtypes @@ -139,10 +140,14 @@ open Refine open Tacinterp open Tacticals open Tactics +open Eqschemes open Cerrors open Class open Command +open Indschemes +open Ind_tables +open Lemmas open Coqinit open Coqtop open Discharge |