diff options
| author | Matthieu Sozeau | 2013-11-04 18:19:28 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:55 +0200 |
| commit | ede4fa2f51bee0a425f68cd159178835a3af3ca6 (patch) | |
| tree | 0cbd06a11bdc25ef4b1d8e81af23f5b5f4cfe9cc /pretyping/evarutil.ml | |
| parent | 7dfb0fb915fa095f8af57e8bb5e4727ebb61304a (diff) | |
Restore reasonable performance by not allocating during universe checks,
using a fast_compare_neq.
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 908e592270..bca599305a 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -126,6 +126,10 @@ let nf_evar_map_undefined evm = (* Auxiliary functions for the conversion algorithms modulo evars *) +let has_flexible_level evd l = + let a = Univ.Instance.to_array l in + Array.exists (fun l -> Evd.is_flexible_level evd l) a + let has_undefined_evars or_sorts evd t = let rec has_ev t = match kind_of_term t with @@ -138,7 +142,7 @@ let has_undefined_evars or_sorts evd t = | Sort (Type _) (*FIXME could be finer, excluding Prop and Set universes *) when or_sorts -> raise Not_found | Ind (_,l) | Const (_,l) | Construct (_,l) - when l <> Univ.Instance.empty && or_sorts -> raise Not_found + when or_sorts && not (Univ.Instance.is_empty l) (* has_flexible_level evd l *) -> raise Not_found | _ -> iter_constr has_ev t in try let _ = has_ev t in false with (Not_found | NotInstantiatedEvar) -> true |