diff options
| author | Maxime Dénès | 2018-03-04 16:46:49 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-04 16:46:49 +0100 |
| commit | 9cd987a07d3792dc200e15c5e792a25a1a99c9c6 (patch) | |
| tree | efa4cbcd3d3959485e8a2f7b4bbb1d5888603be4 /pretyping | |
| parent | 0a9a45abbd3421f3b2cfc4f6428938898a933ffe (diff) | |
| parent | c7be6d5a1e548fe1fdfc7b3fc248613bfb7fc613 (diff) | |
Merge PR #6876: Unify Const_sorts and Const_type, and remove Vsort
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/vnorm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index c93b41786b..6b7ea2996d 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -141,7 +141,6 @@ and nf_vtype env sigma v = nf_val env sigma v crazy_type and nf_whd env sigma whd typ = match whd with - | Vsort s -> mkSort s | Vprod p -> let dom = nf_vtype env sigma (dom p) in let name = Name (Id.of_string "x") in @@ -182,7 +181,8 @@ and nf_whd env sigma whd typ = let pind = (ind, u) in (mkIndU pind, type_of_ind env pind) in nf_univ_args ~nb_univs mk env sigma stk - | Vatom_stk(Atype u, stk) -> assert false + | Vatom_stk(Asort s, stk) -> + assert (List.is_empty stk); mkSort s | Vuniv_level lvl -> assert false |