From 8dd427c50a84aaba3a4187b214af913f5cff11ae Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 11 Feb 2011 13:28:47 +0000
Subject: In evars_of_term and co, visit array c in Evar(_,c) (sequel to
 r13809)

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

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index d1eb33cd6e..098d0d587a 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1365,10 +1365,10 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
 let evars_of_term c =
   let rec evrec acc c =
     match kind_of_term c with
-    | Evar (n, _) -> Intset.add n acc
+    | Evar (n, l) -> Intset.add n (Array.fold_left evrec acc l)
     | _ -> fold_constr evrec acc c
   in
-    evrec Intset.empty c
+  evrec Intset.empty c
 
 let evars_of_named_context nc =
   List.fold_right (fun (_, b, t) s ->
@@ -1393,7 +1393,8 @@ let evars_of_evar_info evi =
 let undefined_evars_of_term evd t =
   let rec evrec acc c =
     match kind_of_term c with
-      | Evar (n, _) -> (* TODO: should we look in the constr array ?? *)
+      | Evar (n, l) ->
+	let acc = Array.fold_left evrec acc l in
 	(try match (Evd.find evd n).evar_body with
 	  | Evar_empty -> Intset.add n acc
 	  | Evar_defined c -> evrec acc c
-- 
cgit v1.2.3