fixed problem with r11612

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

1 files changed, 16 insertions, 1 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index e24cf62bb1..daa0701b08 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -607,8 +607,23 @@ let pb_equal = function
 
 let sort_cmp = sort_cmp
 
+
+let nf_red_env sigma env =
+  let nf_decl = function
+      (x,Some t,ty) -> (x,Some (nf_evar sigma t),ty)
+    | d -> d in
+  let sign = named_context env in
+  let ctxt = rel_context env in
+  let env = reset_context env in
+  let env = Sign.fold_named_context
+    (fun d env -> push_named (nf_decl d) env) ~init:env sign in
+  Sign.fold_rel_context
+    (fun d env -> push_rel (nf_decl d) env) ~init:env ctxt
+
+
 let test_conversion f env sigma x y =
-  try let _ = f env (nf_evar sigma x) (nf_evar sigma y) in true
+  try let _ =
+    f (nf_red_env sigma env) (nf_evar sigma x) (nf_evar sigma y) in true
   with NotConvertible -> false
 
 let is_conv env sigma = test_conversion Reduction.conv env sigma