diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-02 17:48:56 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-02 18:12:00 +0200 |
commit | 1210d1270a7de98abf90761e531062679fb8bdab (patch) | |
tree | c891307717b2f32114cc26ebc8b6f78eebb2b5b5 /engine | |
parent | f60d849a9601febc35a35204d2442e72673e3fb4 (diff) |
Fast path in whd_evar.
Before computing the whd_evar-form of the arguments of an evar, we first
check that it is indeed defined.
Diffstat (limited to 'engine')
-rw-r--r-- | engine/evarutil.ml | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index bd86f4bd2..caf345b5d 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -18,6 +18,10 @@ open Environ open Evd open Sigma.Notations +let safe_evar_info sigma evk = + try Some (Evd.find sigma evk) + with Not_found -> None + let safe_evar_value sigma ev = try Some (Evd.existential_value sigma ev) with NotInstantiatedEvar | Not_found -> None @@ -66,12 +70,14 @@ let rec flush_and_check_evars sigma c = let rec whd_evar sigma c = match kind_of_term c with - | Evar ev -> - let (evk, args) = ev in + | Evar (evk, args) -> + begin match safe_evar_info sigma evk with + | Some ({ evar_body = Evar_defined c } as info) -> let args = Array.map (fun c -> whd_evar sigma c) args in - (match safe_evar_value sigma (evk, args) with - Some c -> whd_evar sigma c - | None -> c) + let c = instantiate_evar_array info c args in + whd_evar sigma c + | _ -> c + end | Sort (Type u) -> let u' = Evd.normalize_universe sigma u in if u' == u then c else mkSort (Sorts.sort_of_univ u') |