diff options
Diffstat (limited to 'dev/base_include')
| -rw-r--r-- | dev/base_include | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include index 7ec0bf4938..71ccea9693 100644 --- a/dev/base_include +++ b/dev/base_include @@ -80,6 +80,7 @@ open Pattern open Patternops open Cbv open Classops +open Arguments_renaming open Pretyping open Cbv open Classops @@ -103,7 +104,15 @@ open Namegen open Indrec open Typing open Inductiveops +open Locusops +open Find_subterm open Unification +open Miscops +open Miscops +open Nativenorm +open Typeclasses +open Typeclasses_errors +open Vnorm open Constrextern open Constrintern @@ -123,14 +132,20 @@ open Prettyp open Search open Evar_refiner +open Goal open Logic open Pfedit +open Proof +open Proofview +open Proof_using +open Proof_global open Proof_type open Redexpr open Refiner open Tacmach -open Decl_proof_instr open Tactic_debug + +open Decl_proof_instr open Decl_mode open Auto |