aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/evd.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/evd.mli')
-rw-r--r--kernel/evd.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/evd.mli b/kernel/evd.mli
index df80ee72b..62378f921 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -10,8 +10,8 @@ open Environ
(* The type of mappings for existential variables.
The keys are integers and the associated information is a record
- containing the type of the evar ([concl]), the signature under which
- it was introduced ([hyps]) and its definition ([body]).
+ containing the type of the evar ([evar_concl]), the environment under which
+ it was introduced ([evar_env]) and its definition ([evar_body]).
[evar_info] is used to add any other kind of information. *)
type evar = int