From d4a81ee817a1a4dbf23d3777be3dff29b96c89db Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 8 May 2014 13:59:34 +0200
Subject: Cleanup code in pretyping/evarutil

---
 pretyping/evarutil.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 510e79bccf..d6b18175b4 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -139,10 +139,9 @@ let has_undefined_evars or_sorts evd t =
             has_ev c; Array.iter has_ev args
         | Evar_empty ->
 	    raise NotInstantiatedEvar)
-    (* | Sort (Type _) (\*FIXME could be finer, excluding Prop and Set universes *\) when or_sorts -> *)
-    (*   raise Not_found *)
     | Ind (_,l) | Const (_,l) | Construct (_,l) 
-	when or_sorts && not (Univ.Instance.is_empty l) (* has_flexible_level evd l *) -> raise Not_found
+	when or_sorts && not (Univ.Instance.is_empty l) -> 
+      raise Not_found
     | _ -> iter_constr has_ev t in
   try let _ = has_ev t in false
   with (Not_found | NotInstantiatedEvar) -> true
-- 
cgit v1.2.3