From 84c0f274e3baa424299c7b098ad7ced9ea4bab0e Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 6 Dec 1999 15:07:11 +0000
Subject: declarations eliminations / debuggae inductifs (debut)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@212 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/typeops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 7066462452..a12c6803ad 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -930,8 +930,8 @@ let type_fixpoint env sigma lna lar vdefj =
   assert (Array.length lar = lt);
   try
     conv_forall2_i
-      (fun i e def ar -> 
-	 try conv_leq e def (lift lt ar) 
+      (fun i env sigma def ar -> 
+	 try conv_leq env sigma def (lift lt ar) 
 	 with NotConvertible -> raise (IllBranch i))
       env sigma
       (Array.map (fun j -> j.uj_type) vdefj) (Array.map body_of_type lar)
-- 
cgit v1.2.3