diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 80dba10682..7908c26f26 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -3,7 +3,6 @@ (*i*) open Names -(* open Generic *) open Term open Univ open Evd |