From afd11e5bfab001ed50381de5f15493fd76894f6b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 13 Dec 2001 16:21:53 +0000
Subject: Contournement du problème des evars de type, typées par défaut dans
 Type (suite)

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

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 3239f0914d..80a4a2ec09 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -354,8 +354,8 @@ let rec pretype tycon env isevars lvar lmeta = function
 		    let pty =
                       Retyping.get_type_of env (evars_of isevars) pred in
 		    let pj = { uj_val = pred; uj_type = pty } in
-                    option_app (the_conv_x_leq env isevars pred) tycon;
-                    pj
+                    let _ = option_app (the_conv_x_leq env isevars pred) tycon
+                    in pj
 		with UserError _ -> findtype (i+1) in
 	    findtype 0 in
       let pj = j_nf_evar (evars_of isevars) pj in
-- 
cgit v1.2.3