diff options
Diffstat (limited to 'pretyping/evardefine.ml')
| -rw-r--r-- | pretyping/evardefine.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 18dbbea1b..b646a37f8 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Sorts open Util open Pp open Names -open Term open Constr open Termops open EConstr |