diff options
| author | Matthieu Sozeau | 2014-04-07 16:31:56 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:59 +0200 |
| commit | 2844926420c4a8436ce04711148a717c296c7236 (patch) | |
| tree | e8f4d6015c5c7d070dcedf080dfe56ff52fdee81 /pretyping | |
| parent | 484e2c349e68b0284f278f691334d82001ee0f0e (diff) | |
Allow records whose sort is defined by a constant.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/retyping.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 4ba6b01dc8..c967bc7ad1 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -76,11 +76,6 @@ let sort_of_atomic_type env sigma ft args = | _ -> retype_error NotASort in concl_of_arity env ft (Array.to_list args) -let decomp_sort env sigma t = - match kind_of_term (whd_betadeltaiota env sigma t) with - | Sort s -> s - | _ -> retype_error NotASort - let type_of_var env id = try let (_,_,ty) = lookup_named id env in ty with Not_found -> retype_error (BadVariable id) |