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 | |
| parent | 484e2c349e68b0284f278f691334d82001ee0f0e (diff) | |
Allow records whose sort is defined by a constant.
| -rw-r--r-- | pretyping/retyping.ml | 5 | ||||
| -rw-r--r-- | toplevel/record.ml | 6 |
2 files changed, 2 insertions, 9 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) diff --git a/toplevel/record.ml b/toplevel/record.ml index c4a4951b3c..71f0175985 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -111,14 +111,12 @@ let typecheck_params_and_fields def id t ps nots fs = let arity = nf t' in let evars = let _, univ = compute_constructor_level evars env_ar newfs in - let aritysort = destSort arity in + let ctx, aritysort = Reduction.dest_arity env0 arity in + assert(List.is_empty ctx); (* Ensured by above analysis *) if Sorts.is_prop aritysort || (Sorts.is_set aritysort && engagement env0 = Some ImpredicativeSet) then evars else Evd.set_leq_sort evars (Type univ) aritysort - (* try Evarconv.the_conv_x_leq env_ar ty arity evars *) - (* with Reduction.NotConvertible -> *) - (* Pretype_errors.error_cannot_unify env_ar evars (ty, arity) *) in let evars, nf = Evarutil.nf_evars_and_universes evars in let newps = map_rel_context nf newps in |