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.

5 files changed, 42 insertions, 30 deletions

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 637e0e28d5..2a2ef30fb1 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -211,9 +211,9 @@ let compute_rhs bodyi index_of_f =
           let i = destRel (Array.last args) in
 	  PMeta (Some (coerce_meta_in i))
       | App (f,args) ->
-          PApp (snd (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args)
+          PApp (pi3 (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args)
       | Cast (c,_,_) -> aux c
-      | _ -> snd (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
+      | _ -> pi3 (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
   in
   aux bodyi
 
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
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index cf02421c24..9e72280fe2 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -39,7 +39,8 @@ val head_of_constr_reference : Term.constr -> global_reference
    a pattern; currently, no destructor (Cases, Fix, Cofix) and no
    existential variable are allowed in [c] *)
 
-val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> named_context * constr_pattern
+val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> 
+  Evd.evar_map * named_context * constr_pattern
 
 (** [pattern_of_glob_constr l c] translates a term [c] with metavariables into
    a pattern; variables bound in [l] are replaced by the pattern to which they
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 5621c365aa..101223b570 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -609,7 +609,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
     match kind_of_term cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
-	let pat = snd (Patternops.pattern_of_constr env sigma cty) in
+	let pat = pi3 (Patternops.pattern_of_constr env sigma cty) in
 	let hd =
 	  try head_pattern_bound pat
 	  with BoundPattern -> failwith "make_exact_entry"
@@ -628,7 +628,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
         let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
         let ce = mk_clenv_from_env env sigma' None (c,cty) in
 	let c' = clenv_type (* ~reduce:false *) ce in
-	let pat = snd (Patternops.pattern_of_constr env ce.evd c') in
+	let pat = pi3 (Patternops.pattern_of_constr env ce.evd c') in
         let hd =
 	  try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry" in
@@ -726,7 +726,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
 	      poly = poly;
-              pat = Some (snd (Patternops.pattern_of_constr env ce.evd (clenv_type ce)));
+              pat = Some (pi3 (Patternops.pattern_of_constr env ce.evd (clenv_type ce)));
 	      name = name;
               code=Res_pf_THEN_trivial_fail(c,t,ctx) })
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8826875a38..1429211f19 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -681,7 +681,7 @@ let interp_constr_with_occurrences ist env sigma (occs,c) =
 let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
   let p = match a with
   | Inl b -> Inl (interp_evaluable ist env sigma b)
-  | Inr c -> Inr (snd (interp_typed_pattern ist env sigma c)) in
+  | Inr c -> Inr (pi3 (interp_typed_pattern ist env sigma c)) in
   interp_occurrences ist occs, p
 
 let interp_constr_with_occurrences_and_name_as_list =
@@ -1030,7 +1030,7 @@ let use_types = false
 
 let eval_pattern lfun ist env sigma (_,pat as c) =
   if use_types then
-    snd (interp_typed_pattern ist env sigma c)
+    pi3 (interp_typed_pattern ist env sigma c)
   else
     instantiate_pattern env sigma lfun pat
 
@@ -2138,7 +2138,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         Proofview.V82.tactic begin fun gl -> 
-          let sign,op = interp_typed_pattern ist env sigma op in
+          let (sigma,sign,op) = interp_typed_pattern ist env sigma op in
           let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
 	  let env' = Environ.push_named_context sign env in
           let c_interp sigma =
@@ -2146,8 +2146,8 @@ and interp_atomic ist tac : unit Proofview.tactic =
 	      with e when to_catch e (* Hack *) ->
 		errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
           in
-	      (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl))
-		gl
+	    (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl))
+	      { gl with sigma = sigma }
         end
       end
       end