From 90eea6b18bd76e840a5bf364230049700575d042 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 13 May 2003 22:18:16 +0000
Subject: Rien d'important

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

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index cb224fac23..e4714468ae 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -185,7 +185,7 @@ let make_dep_of_undep env (IndType (indf,realargs)) pj =
 (*************************************************************************)
 (* Main pretyping function                                               *)
 
-let pretype_ref isevars env lvar ref = 
+let pretype_ref isevars env ref = 
   let c = constr_of_reference ref in
   make_judge c (Retyping.get_type_of env Evd.empty c)
 
@@ -200,7 +200,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 
   | RRef (loc,ref) ->
       inh_conv_coerce_to_tycon loc env isevars
-	(pretype_ref isevars env lvar ref)
+	(pretype_ref isevars env ref)
 	tycon
 
   | RVar (loc, id) ->
-- 
cgit v1.2.3