aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-02 17:48:56 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-02 18:12:00 +0200
commit1210d1270a7de98abf90761e531062679fb8bdab (patch)
treec891307717b2f32114cc26ebc8b6f78eebb2b5b5 /engine
parentf60d849a9601febc35a35204d2442e72673e3fb4 (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.ml16
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')