fixed problem with r11612

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

5 files changed, 49 insertions, 5 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 2ac913607a..46969ec831 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -1145,7 +1145,21 @@ let array_fold_map2' f v1 v2 e =
   in
   (v',!e')
 
+(* N.logN *)
 let array_distinct v =
+  let visited = Hashtbl.create 23 in
+  try
+    Array.iter
+      (fun x ->
+        if Hashtbl.mem visited h then raise Exit
+        else Hashtbl.add visited h h)
+      v;
+    true
+  with Exit -> false
+
+
+(* quadratic *)
+(*let array_distinct v =
   try
     for i=0 to Array.length v-1 do
       for j=i+1 to Array.length v-1 do
@@ -1155,6 +1169,7 @@ let array_distinct v =
     true
   with Exit ->
     false
+*)
 
 let array_union_map f a acc =
   Array.fold_left
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index efbe2f3358..6664939fbb 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -165,8 +165,8 @@ let rec evar_conv_x env evd pbty term1 term2 =
      could have found, we do it only if the terms are free of evar.
      Note: incomplete heuristic... *)
   if is_ground_term evd term1 && is_ground_term evd term2
-  then
-    (evd,is_fconv pbty env (evars_of evd) term1 term2)
+    && is_ground_env evd env
+  then (evd, is_fconv pbty env (evars_of evd) term1 term2)
   else
   let term1 = apprec_nohdbeta env evd term1 in
   let term2 = apprec_nohdbeta env evd term2 in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 733aa9613b..551db4e4fa 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -258,13 +258,19 @@ let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ty =
  * operations on the evar constraints *
  *------------------------------------*)
 
+let is_pattern inst =
+  array_for_all (fun a -> isRel a || isVar a) inst &&
+  array_distinct inst
+
 (* Pb: defined Rels and Vars should not be considered as a pattern... *)
+(*
 let is_pattern inst =
   let rec is_hopat l = function
       [] -> true
     | t :: tl ->
         (isRel t or isVar t) && not (List.mem t l) && is_hopat (t::l) tl in
   is_hopat [] (Array.to_list inst)
+*)
 
 let evar_well_typed_body evd ev evi body =
   try
@@ -940,6 +946,13 @@ let has_undefined_evars evd t =
 let is_ground_term evd t =
   not (has_undefined_evars evd t)
 
+let is_ground_env evd env =
+  let is_ground_decl = function
+      (_,Some b,_) -> is_ground_term evd b
+    | _ -> true in
+  List.for_all is_ground_decl (rel_context env) &&
+  List.for_all is_ground_decl (named_context env)
+
 let head_evar = 
   let rec hrec c = match kind_of_term c with
     | Evar (evk,_)   -> evk
@@ -957,11 +970,11 @@ let head_evar =
 let is_unification_pattern_evar env (_,args) l =
   let l' = Array.to_list args @ l in
   let l' = List.map (expand_var env) l' in
-  List.for_all (fun a -> isRel a or isVar a) l' & list_distinct l'
+  List.for_all (fun a -> isRel a or isVar a) l' && list_distinct l'
 
 let is_unification_pattern env f l =
   match kind_of_term f with
-    | Meta _ -> array_for_all isRel l & array_distinct l
+    | Meta _ -> array_for_all isRel l && array_distinct l
     | Evar ev -> is_unification_pattern_evar env ev (Array.to_list l)
     | _ -> false
 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index ab9f8bebb1..3ed39fc19c 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -73,6 +73,7 @@ val non_instantiated : evar_map -> (evar * evar_info) list
 (* Unification utils *)
 
 val is_ground_term :  evar_defs -> constr -> bool
+val is_ground_env  :  evar_defs -> env -> bool
 val solve_refl : 
   (env ->  evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
   -> env ->  evar_defs -> existential_key -> constr array -> constr array ->
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