From 972616f79a627d97788caaab992497cfb7a86a17 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 14 Sep 2000 07:12:52 +0000
Subject: Intégré à Tacred
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@601 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/redinfo.mli | 20 --------------------
 1 file changed, 20 deletions(-)
 delete mode 100644 library/redinfo.mli

(limited to 'library/redinfo.mli')

diff --git a/library/redinfo.mli b/library/redinfo.mli
deleted file mode 100644
index 1b600e57b..000000000
--- a/library/redinfo.mli
+++ /dev/null
@@ -1,20 +0,0 @@
-
-(* $Id$ *)
-
-(*i*)
-open Names
-open Term
-(*i*)
-
-(* Elimination constants. This module implements a table which associates
-   to each constant some reduction informations used by tactics like Simpl. 
-   The following table is mostly used by the module [Tacred] 
-   (section~\refsec{tacred}). *)
-
-type constant_evaluation = 
-  | EliminationFix of (int * constr) list * int
-  | EliminationCases of int
-  | NotAnElimination
-
-val constant_eval : section_path -> constant_evaluation
-
-- 
cgit v1.2.3