Cosmetic code contraction in evarsolve.ml + test sur unification avec let-in.

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

2 files changed, 16 insertions, 12 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index a2eebcc242..50fc91e31e 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -781,7 +781,9 @@ let eq_filter f1 f2 =
   let eq_bool b1 b2 = if b1 then b2 else not b2 in
   List.equal eq_bool f1 f2
 
-let closure_of_filter evd evk filter =
+let closure_of_filter evd evk = function
+  | None -> None
+  | Some filter ->
   let evi = Evd.find_undefined evd evk in
   let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in
   let ids = List.map pi1 (evar_context evi) in
@@ -801,7 +803,7 @@ let restrict_hyps evd evk filter candidates =
        it for future work. In any case, thanks to the use of filters, the whole
        (unrestricted) context remains consistent. *)
     let candidates = filter_candidates evd evk (Some filter) candidates in
-    let typablefilter = closure_of_filter evd evk filter in
+    let typablefilter = closure_of_filter evd evk (Some filter) in
     (typablefilter,candidates)
 
 exception EvarSolvedWhileRestricting of evar_map * constr
@@ -828,16 +830,14 @@ let postpone_non_unique_projection env evd (evk,argsv as ev) sols rhs =
       (* Keep only variables that occur in rhs *)
       (* This is not safe: is the variable is a local def, its body *)
       (* may contain references to variables that are removed, leading to *)
-      (* a ill-formed context. We would actually need a notion of filter *)
+      (* an ill-formed context. We would actually need a notion of filter *)
       (* that says that the body is hidden. Note that expand_vars_in_term *)
       (* expands only rels and vars aliases, not rels or vars bound to an *)
       (* arbitrary complex term *)
       (fun a -> not (isRel a || isVar a)
                 || dependent a rhs || List.exists (fun (id,_) -> isVarId id a) sols)
       (Array.to_list argsv) in
-  let filter = match filter with
-  | None -> None
-  | Some filter -> closure_of_filter evd evk filter in
+  let filter = closure_of_filter evd evk filter in
   let candidates = extract_candidates sols in
   match candidates with
   | None ->
@@ -1065,9 +1065,7 @@ let solve_refl ?(can_drop=false) conv_algo env evd evk argsv1 argsv2 =
       (fun (a1,a2) -> conv_algo env evd Reduction.CONV a1 a2)
       (List.combine (Array.to_list argsv1) (Array.to_list argsv2)) in
   let candidates = filter_candidates evd evk untypedfilter None in
-  let filter = match untypedfilter with
-    | None -> None
-    | Some filter -> closure_of_filter evd evk filter in
+  let filter = closure_of_filter evd evk untypedfilter in
   let evd,ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in
   if Int.equal (fst ev1) evk && can_drop then (* No refinement *) evd else
     (* either progress, or not allowed to drop, e.g. to preserve possibly *)
@@ -1168,9 +1166,8 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
             materialize_evar (evar_define conv_algo) env !evdref 0 ev ty' in
           let ts = expansions_of_var aliases t in
           let test c = isEvar c or List.mem c ts in
-          let filter = Array.map_to_list test argsv' in
-          let filter = apply_subfilter (evar_filter (Evd.find_undefined evd evk)) filter in
-
+          let filter =
+            restrict_upon_filter evd evk test (Array.to_list argsv') in
           let filter = closure_of_filter evd evk' filter in
           let candidates = extract_candidates sols in
           let evd = match candidates with
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 4c77e4bcfd..ef2164a942 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -392,3 +392,10 @@ Definition tri_iffT : tri iffT iffT iffT :=
     (fun X0 X1 X2 E01 E02 =>
      (mkIff _ _ (fun x1 => iffLR _ _ E02 (iffRL _ _ E01 x1))
      (fun x2 => iffLR _ _ E01 (iffRL _ _ E02 x2))))).
+
+(* Check that local defs names are preserved if possible during unification *)
+
+Goal forall x (x':=x) (f:forall y, y=y:>nat -> Prop), f _ (eq_refl x').
+intros.
+unfold x' at 2. (* A way to check that there are indeed 2 occurrences of x' *)
+Abort.