diff options
Diffstat (limited to 'pretyping/evardefine.ml')
| -rw-r--r-- | pretyping/evardefine.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index c5ae684e3..5fd104c78 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -11,7 +11,6 @@ open Pp open Names open Term open Termops -open Environ open EConstr open Vars open Namegen |