blob: 3f71baa9826264399f84e2ab1c1c0b1bc6a10b5c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(* $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 =
| Elimination of (int * constr) list * int * bool
| NotAnElimination
val constant_eval : section_path -> constant_evaluation
|
