From 0e69a26eadeabf5987aacdac57cd6a5b90b0cdc8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 11 May 2013 16:14:13 +0000
Subject: Fixing a source of evars leak, revealed by contrib
 QuicksortComplexity after r16499 which replaced a check for visible undefined
 evars (check_evars) by a check for undefined evars in the evar map
 (check_evars_are_solved).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16508 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/cases.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index d942ba0d04..ade4598e89 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1355,17 +1355,20 @@ and compile_alias pb (na,orig,(expanded,expanded_typ)) rest =
         else
           mkLetIn (na,c,t,j.uj_val);
       uj_type = subst1 c j.uj_type } in
+  let sigma = !(pb.evdref) in
   if not (Flags.is_program_mode ()) && (isRel orig or isVar orig) then
     (* Try to compile first using non expanded alias *)
     try f orig (Retyping.get_type_of pb.env !(pb.evdref) orig)
     with e when precatchable_exception e ->
     (* Try then to compile using expanded alias *)
+    pb.evdref := sigma;
     f expanded expanded_typ
   else
     (* Try to compile first using expanded alias *)
     try f expanded expanded_typ
     with e when precatchable_exception e ->
     (* Try then to compile using non expanded alias *)
+    pb.evdref := sigma;
     f orig (Retyping.get_type_of pb.env !(pb.evdref) orig)
 
 
-- 
cgit v1.2.3