diff options
| -rw-r--r-- | pretyping/evarutil.ml | 5 |
1 files 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 |