From 2844926420c4a8436ce04711148a717c296c7236 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Apr 2014 16:31:56 +0200
Subject: Allow records whose sort is defined by a constant.

---
 pretyping/retyping.ml | 5 -----
 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
-- 
cgit v1.2.3