Like in r16346, do not filter local definitions (here in the

type-based second-order unification algorithm).

In type-based second-order unification algorithm, protect local
definitions in instances of evars to wrongly be considered as
potentially flexible.

Altogether, this fixes the anomaly in #3003 (even if some additional
work has to be done to improve the resulting error message, see next
commit).

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

1 files changed, 12 insertions, 5 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 8da09d5c5..c4d1a72e6 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -629,15 +629,21 @@ let choose_less_dependent_instance evk evd term args =
   | [] -> None
   | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd)
 
-let apply_on_subterm f c t =
+let apply_on_subterm evdref f c t =
   let rec applyrec (k,c as kc) t =
     (* By using eq_constr, we make an approximation, for instance, we *)
     (* could also be interested in finding a term u convertible to t *)
     (* such that c occurs in u *)
     if eq_constr c t then f k
     else
-      map_constr_with_binders_left_to_right (fun d (k,c) -> (k+1,lift 1 c))
-	applyrec kc t
+      match kind_of_term t with
+      | Evar (evk,args) when Evd.is_undefined !evdref evk ->
+          let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in
+          let g (_,b,_) a = if b = None then applyrec kc a else a in
+          mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args)))
+      | _ ->
+        map_constr_with_binders_left_to_right (fun d (k,c) -> (k+1,lift 1 c))
+	  applyrec kc t
   in
   applyrec (0,c) t
 
@@ -645,7 +651,8 @@ let filter_possible_projections c ty ctxt args =
   let fv1 = free_rels c in
   let fv2 = collect_vars c in
   let tyvars = collect_vars ty in
-  List.map2 (fun (id,_,_) a ->
+  List.map2 (fun (id,b,_) a ->
+    b <> None ||
     a == c ||
     (* Here we make an approximation, for instance, we could also be *)
     (* interested in finding a term u convertible to c such that a occurs *)
@@ -717,7 +724,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
         evdref := evd;
         evsref := (fst (destEvar ev),evty)::!evsref;
         ev in
-      set_holes evdref (apply_on_subterm set_var c rhs) subst
+      set_holes evdref (apply_on_subterm evdref set_var c rhs) subst
   | [] -> rhs in
 
   let subst = make_subst (ctxt,args,argoccs) in