From 0b3a335219e161dc04f6734e9ee4f7c08cde6cd5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Jul 2015 21:34:08 +0200
Subject: Fixing #4177 (find_projectable was liable to ask to instantiate an
 evar twice).

This is a bug in a pretty old code, showing also in 8.3 and 8.4.
---
 pretyping/evarsolve.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b2cf21b818..ac1692f451 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -694,7 +694,8 @@ let rec find_projectable_vars with_evars aliases sigma y subst =
     (* Then test if [idc] is (indirectly) bound in [subst] to some evar *)
     (* projectable on [y] *)
       if with_evars then
-        let idcl' = List.filter (fun (c,_,id) -> isEvar c) idcl in
+        let f (c,_,id) = isEvar c && is_undefined sigma (fst (destEvar c)) in
+        let idcl' = List.filter f idcl in
         match idcl' with
         | [c,_,id] ->
           begin
-- 
cgit v1.2.3