From 00df263febb97990d6c29a6aaf4504e059ebf68c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 21 Jan 2006 20:05:56 +0000
Subject: Variable inutilisée

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

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 06a3d5ecf2..92b919c7eb 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -171,7 +171,6 @@ let is_correct_arity env c pj ind mib mip params =
   let kelim = mip.mind_kelim in
   let arsign,s = get_arity mib mip params in
   let nodep_ar = it_mkProd_or_LetIn (mkSort s) arsign in
-  let nrealargs = mip.mind_nrealargs in
   let rec srec env pt t u =
     let pt' = whd_betadeltaiota env pt in
     let t' = whd_betadeltaiota env t in
-- 
cgit v1.2.3