summaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
Diffstat (limited to 'dev/base_include')
-rw-r--r--dev/base_include2
1 files changed, 2 insertions, 0 deletions
diff --git a/dev/base_include b/dev/base_include
index de63c557..dac1f609 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -86,6 +86,7 @@ open Cbv
open Classops
open Clenv
open Clenvtac
+open Constr_matching
open Glob_term
open Glob_ops
open Coercion
@@ -147,6 +148,7 @@ open Tactic_debug
open Decl_proof_instr
open Decl_mode
+open Hints
open Auto
open Autorewrite
open Contradiction