diff options
| -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 |