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.

2 files changed, 8 insertions, 8 deletions

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