diff options
| author | Matthieu Sozeau | 2014-05-08 13:59:34 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-08 19:23:52 +0200 |
| commit | d4a81ee817a1a4dbf23d3777be3dff29b96c89db (patch) | |
| tree | ad97b6b9b636148a710932678980c927ea9bbe17 | |
| parent | efa11b99cd42d8806645109d96720a4c0c83756c (diff) | |
Cleanup code in pretyping/evarutil
| -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 |