diff options
Diffstat (limited to 'library/redinfo.mli')
| -rw-r--r-- | library/redinfo.mli | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/library/redinfo.mli b/library/redinfo.mli new file mode 100644 index 0000000000..3f71baa982 --- /dev/null +++ b/library/redinfo.mli @@ -0,0 +1,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 + |