Fix bug #3590, keeping evars that are not turned into named metas by

pattern_of_constr in an evar_map, as they can appear in the context
of said named metas, which is used by change. Not sure what to do in
the PEvar case, which never matches anyway according to Constr_matching.matches.

1 files changed, 30 insertions, 19 deletions

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index c49bec9aec..009b7323e4 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -123,6 +123,8 @@ let head_of_constr_reference c = match kind_of_term c with
 
 let pattern_of_constr env sigma t =
   let ctx = ref [] in
+  let keep = ref Evar.Set.empty in
+  let remove = ref Evar.Set.empty in
   let rec pattern_of_constr env t =
   match kind_of_term t with
     | Rel n  -> PRel n
@@ -141,28 +143,35 @@ let pattern_of_constr env sigma t =
     | App (f,a) ->
         (match
           match kind_of_term f with
-            Evar (evk,args as ev) ->
-              (match snd (Evd.evar_source evk sigma) with
-                  Evar_kinds.MatchingVar (true,id) ->
-                    ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx;
-                    Some id
-                | _ -> None)
-            | _ -> None
-          with
-            | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a))
-            | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a))
+          | Evar (evk,args as ev) ->
+            (match snd (Evd.evar_source evk sigma) with
+              Evar_kinds.MatchingVar (true,id) ->
+		let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
+                  ctx := (id,None,ty)::!ctx;
+		  keep := Evar.Set.union (evars_of_term ty) !keep;
+		  remove := Evar.Set.add evk !remove;
+                  Some id
+            | _ -> None)
+          | _ -> None
+         with
+         | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a))
+         | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a))
     | Const (sp,u)  -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
     | Ind (sp,u)    -> PRef (canonical_gr (IndRef sp))
     | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
     | Proj (p, c) -> 
       pattern_of_constr env (Retyping.expand_projection env sigma p c [])
     | Evar (evk,ctxt as ev) ->
-        (match snd (Evd.evar_source evk sigma) with
-          | Evar_kinds.MatchingVar (b,id) ->
-              ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx;
-              assert (not b); PMeta (Some id)
-          | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt)
-          | _ -> PMeta None)
+      remove := Evar.Set.add evk !remove;
+      (match snd (Evd.evar_source evk sigma) with
+      | Evar_kinds.MatchingVar (b,id) ->
+	let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
+          ctx := (id,None,ty)::!ctx;
+	  keep := Evar.Set.union (evars_of_term ty) !keep;
+          assert (not b); PMeta (Some id)
+      | Evar_kinds.GoalEvar -> 
+	PEvar (evk,Array.map (pattern_of_constr env) ctxt)
+      | _ -> PMeta None)
     | Case (ci,p,a,br) ->
         let cip =
 	  { cip_style = ci.ci_pp_info.style;
@@ -178,9 +187,11 @@ let pattern_of_constr env sigma t =
     | Fix f -> PFix f
     | CoFix f -> PCoFix f in
   let p = pattern_of_constr env t in
+  let remove = Evar.Set.diff !remove !keep in
+  let sigma = Evar.Set.fold (fun ev acc -> Evd.remove acc ev) remove sigma in
   (* side-effect *)
   (* Warning: the order of dependencies in ctx is not ensured *)
-  (!ctx,p)
+  (sigma,!ctx,p)
 
 (* To process patterns, we need a translation without typing at all. *)
 
@@ -220,7 +231,7 @@ let instantiate_pattern env sigma lvar c =
               ctx
           in
 	  let c = substl inst c in
-	  snd (pattern_of_constr env sigma c)
+	  pi3 (pattern_of_constr env sigma c)
 	with Not_found (* List.index failed *) ->
 	  let vars =
 	    List.map_filter (function Name id -> Some id | _ -> None) vars in
@@ -245,7 +256,7 @@ let rec subst_pattern subst pat =
   | PRef ref ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then pat else
-	 snd (pattern_of_constr (Global.env()) Evd.empty t)
+	 pi3 (pattern_of_constr (Global.env()) Evd.empty t)
   | PVar _
   | PEvar _
   | PRel _ -> pat