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 735889034..7e1d1c984 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -115,7 +115,7 @@ type instance_constraint =
IsSuperType | IsSubType | ConvUpToEta of int | UserGiven
type instance_typing_status =
- TypeNotProcessed | TypeProcessed
+ CoerceToType | TypeNotProcessed | TypeProcessed
type instance_status = instance_constraint * instance_typing_status