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

2 files changed, 24 insertions, 5 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 8da09d5c56..c4d1a72e62 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
diff --git a/test-suite/bugs/closed/3003.v b/test-suite/bugs/closed/3003.v
new file mode 100644
index 0000000000..2f8bcdae7a
--- /dev/null
+++ b/test-suite/bugs/closed/3003.v
@@ -0,0 +1,12 @@
+(* This used to raise an anomaly in 8.4 and trunk up to 17 April 2013 *)
+
+Set Implicit Arguments.
+
+Inductive path (V : Type) (E : V -> V -> Type) (s : V) : V -> Type :=
+  | NoEdges : path E s s
+  | AddEdge : forall d d' : V, path E s d -> E d d' -> path E s d'.
+Inductive G_Vertex := G_v0 | G_v1.
+Inductive G_Edge : G_Vertex -> G_Vertex -> Set := G_e : G_Edge G_v0 G_v1.
+Goal forall x1 : G_Edge G_v1 G_v1, @AddEdge _ G_Edge G_v1 _ _ (NoEdges _ _) x1 = NoEdges _ _.
+intro x1.
+try destruct x1. (* now raises a typing error *)