diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-11 16:14:13 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-11 16:14:13 +0000 |
| commit | 0e69a26eadeabf5987aacdac57cd6a5b90b0cdc8 (patch) | |
| tree | 2657903bc5c4c9bd4a78e7e68ad8658ddb10255a | |
| parent | 318c4ba9825b32e41d354473496926f081ea1a52 (diff) | |
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
| -rw-r--r-- | pretyping/cases.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index d942ba0d0..ade4598e8 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) |