From 6170732204b21f982cc6e0ef3e0931add3576d6b Mon Sep 17 00:00:00 2001
From: puech
Date: Fri, 29 Jul 2011 14:25:16 +0000
Subject: Class: generic equality on constr replaced by destructors

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14324 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/class.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 4e729f4460..e977959d2d 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -92,7 +92,9 @@ let check_target clt = function
 let uniform_cond nargs lt =
   let rec aux = function
     | (0,[]) -> true
-    | (n,t::l) -> (strip_outer_cast t = mkRel n) & (aux ((n-1),l))
+    | (n,t::l) ->
+      let t = strip_outer_cast t in
+      isRel t && destRel t = n && aux ((n-1),l)
     | _ -> false
   in
   aux (nargs,lt)
-- 
cgit v1.2.3