aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evd.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evd.mli')
-rw-r--r--pretyping/evd.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index ebf91b4f4..43f214d0d 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -162,7 +162,7 @@ val is_evar : evar_map -> evar -> bool
val is_defined : evar_map -> evar -> bool
-(** {6 Sect } *)
+(** {6 ... } *)
(** [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
no body and [Not_found] if it does not exist in [sigma] *)