blob: 1b600e57b33d9f7166f86e59ef68c94a3ef5ec28 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
(* $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
|
