From 34aeda3d701efd5dead8890588fb02bcdb4980d2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 17 Jun 2020 15:10:32 +0200
Subject: Merge Clenvtac into Clenv.

Having two different modules led to the availability of internal API in
the mli.
---
 dev/base_include | 1 -
 1 file changed, 1 deletion(-)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index 45e79147c1..efbd156758 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -66,7 +66,6 @@ open Pretyping
 open Cbv
 open Coercionops
 open Clenv
-open Clenvtac
 open Constr_matching
 open Glob_term
 open Glob_ops
-- 
cgit v1.2.3