diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-14 07:12:52 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-14 07:12:52 +0000 |
| commit | 972616f79a627d97788caaab992497cfb7a86a17 (patch) | |
| tree | 5b1d8d17f4795f521375f3050ed996db67bfad24 /library/redinfo.mli | |
| parent | 148aee35615772086a8dc511f3b42a7768c9f2a5 (diff) | |
Intégré à Tacred
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@601 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/redinfo.mli')
| -rw-r--r-- | library/redinfo.mli | 20 |
1 files changed, 0 insertions, 20 deletions
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 - |