From 51d4da4ac126b4b3bb033ec88253866345594e01 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 25 Nov 2013 14:25:29 +0100
Subject: Remove the Hiddentac module.

Since the new proof engine, Hiddentac has been essentially trivial.
Here is what happened to the functions defined there
- Aliases, or tactics that were trivial to inline were systematically inlined
- Tactics used only in tacinterp have been moved to tacinterp
- Other tactics have been moved to a new module Tactics.Simple.
---
 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 87c0e5b7e9..94146102be 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -136,7 +136,6 @@ open Equality
 open Evar_tactics
 open Extraargs
 open Extratactics
-open Hiddentac
 open Hipattern
 open Inv
 open Leminv
-- 
cgit v1.2.3