From 3e7c148472265c6066633bf39a63bfe387ba9351 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 6 Jul 2012 11:24:29 +0000
Subject: Fixes bug #2678

Some "dependent evars" were forgotten in the emacs mode.

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

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index b8f216ad42..7a9b415598 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1804,7 +1804,11 @@ let rec add_evars_of_evars_in_types_of_set acc evm s =
     let r = add_evars_of_evars_in_type r evm e in
     match (Evd.find evm e).evar_body with
     | Evar_empty -> r
-    | Evar_defined b -> add_evars_of_evars_in_types_of_set r evm (evars_of_term b)
+    | Evar_defined b ->
+        (* Adds the evars used to define [b] to the binding map. *)
+        let r = add_evars_of_evars_of_term r evm b in
+        (* Goes recursively in the [evar_info] of each of these evar. *)
+        add_evars_of_evars_in_types_of_set r evm (evars_of_term b)
   end s acc
 
 let evars_of_evars_in_types_of_list evm l =
-- 
cgit v1.2.3