diff options
| author | Hugo Herbelin | 2014-10-31 17:28:42 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-31 18:49:05 +0100 |
| commit | 801cd9cb0559d3b78216da166044bd02348ed9af (patch) | |
| tree | f772b921179bf31dae0ebe48caa3a946553261de /dev | |
| parent | cc27d50bf7423fe1df00330eddcd81d18b55fd0f (diff) | |
More "open" by default for trace debugging.
Diffstat (limited to 'dev')
| -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 |