diff options
Diffstat (limited to 'engine/evarutil.mli')
| -rw-r--r-- | engine/evarutil.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli index ffff2c5dd9..111d0f3e8c 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -11,7 +11,7 @@ open Term open Evd open Environ -(** {5 This modules provides useful functions for unification modulo evars } *) +(** This module provides useful higher-level functions for evar manipulation. *) (** {6 Metas} *) |