diff options
| author | Gaëtan Gilbert | 2018-06-11 13:57:28 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 15:46:16 +0100 |
| commit | 06b29ed748a9d9b99c2c08a3788906dbad5417d2 (patch) | |
| tree | 5623fad28f68f9450ab7122f595ec1727f8f52bf /kernel/mod_typing.ml | |
| parent | 71b9ad8526155020c8451dd326a52e391a9a8585 (diff) | |
Repair relevance marks in-kernel.
Prevent errors when under annotating binders.
Diffstat (limited to 'kernel/mod_typing.ml')
| -rw-r--r-- | kernel/mod_typing.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 421d932d9a..2de5faa6df 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -80,6 +80,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let c',cst = match cb.const_body with | Undef _ | OpaqueDef _ -> let j = Typeops.infer env' c in + assert (j.uj_val == c); (* relevances should already be correct here *) let typ = cb.const_type in let cst' = Reduction.infer_conv_leq env' (Environ.universes env') j.uj_type typ in @@ -101,6 +102,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let cst = match cb.const_body with | Undef _ | OpaqueDef _ -> let j = Typeops.infer env' c in + assert (j.uj_val == c); (* relevances should already be correct here *) let typ = cb.const_type in let cst' = Reduction.infer_conv_leq env' (Environ.universes env') j.uj_type typ in |