Réduire pour trouver l'arité d'une classe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6355 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 7 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index c9ed58c79..355cdbc9c 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -92,15 +92,12 @@ let explain_coercion_error g = function
 
 (* Verifications pour l'ajout d'une classe *)
 
-let rec arity_sort a = match kind_of_term a with
-  | Sort (Prop _ | Type _) -> 0
-  | Prod (_,_,c) -> (arity_sort c) +1
-  | LetIn (_,_,_,c) -> arity_sort c    (* Utile ?? *)
-  | Cast (c,_) -> arity_sort c
-  | _ -> raise Not_found
+let rec arity_sort (ctx,a) = match kind_of_term a with
+  | Sort (Prop _ | Type _) -> List.length ctx
 
 let check_reference_arity ref =
-  try arity_sort (Global.type_of_global ref)
+  let t = Global.type_of_global ref in
+  try arity_sort (Reductionops.splay_prod (Global.env()) Evd.empty t)
   with Not_found -> raise (CoercionError (NotAClass ref))
 
 let check_arity = function