Passage à des contextes de vars et de rels pouvant contenir des déclarations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 3 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 8276188566..4c2cbf9873 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -33,10 +33,9 @@ type 'a clausenv = {
 type wc = walking_constraints
 
 let new_evar_in_sign env =
-  let hyps = Environ.var_context env in
+  let ids = ids_of_var_context (Environ.var_context env) in
   let ev = new_evar () in
-  DOPN(Evar ev,
-       Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps)))
+  DOPN(Evar ev, Array.of_list (List.map (fun id -> VAR id) ids))
 
 let rec whd_evar env sigma = function
   | DOPN(Evar ev,_) as k ->