From 1210d1270a7de98abf90761e531062679fb8bdab Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 2 Sep 2016 17:48:56 +0200
Subject: 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.
---
 engine/evarutil.ml | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

(limited to 'engine')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index bd86f4bd27..caf345b5d6 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')
-- 
cgit v1.2.3