From be1619398f5b4802ebe765abf1c0c5aa27fd11bc Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 24 Feb 2011 15:48:27 +0000
Subject: Mod_subst: improving sharing of subst_mps

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13854 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/declarations.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 282dad0da..fc8064d59 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -210,7 +210,7 @@ type mutual_inductive_body = {
   }
 
 let subst_arity sub arity =
-  if sub = empty_subst then arity
+  if is_empty_subst sub then arity
   else match arity with
     | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s)
     | PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s)
-- 
cgit v1.2.3