Fix bug #4433, removing hack on evars appearing in a pattern from a

constr, and the associated signature, not needed anymore.
Update CHANGES, no evar_map is produced by pattern_of_constr anymore.

6 files changed, 18 insertions, 36 deletions

diff --git a/CHANGES b/CHANGES
index 719be44929..07d6281717 100644
--- a/CHANGES
+++ b/CHANGES
@@ -107,8 +107,6 @@ API
 
 - The interface of [change] has changed to take a [change_arg], which
   can be built from a [constr] using [make_change_arg].
-- [pattern_of_constr] now returns a triplet including the cleaned-up
-  [evar_map], removing the evars that were turned into metas.
 
 Changes from V8.4 to V8.5beta1
 ==============================
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 2a2ef30fb1..b72ebbc927 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 (pi3 (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args)
+          PApp (pattern_of_constr (Global.env()) Evd.empty f, Array.map aux args)
       | Cast (c,_,_) -> aux c
-      | _ -> pi3 (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
+      | _ -> pattern_of_constr (Global.env())(*FIXME*) Evd.empty c
   in
   aux bodyi
 
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index fb629d049f..83bf355cc2 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -122,9 +122,6 @@ let head_of_constr_reference c = match kind_of_term c with
   | _ -> anomaly (Pp.str "Not a rigid reference")
 
 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
@@ -143,14 +140,9 @@ let pattern_of_constr env sigma t =
     | App (f,a) ->
         (match
           match kind_of_term f with
-          | Evar (evk,args as ev) ->
+          | Evar (evk,args) ->
             (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
+              Evar_kinds.MatchingVar (true,id) -> Some id
             | _ -> None)
           | _ -> None
          with
@@ -162,13 +154,11 @@ let pattern_of_constr env sigma t =
     | Proj (p, c) -> 
       pattern_of_constr env (Retyping.expand_projection env sigma p c [])
     | Evar (evk,ctxt as ev) ->
-      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;
-	  let () = ignore (pattern_of_constr env ty) in
-          assert (not b); PMeta (Some id)
+	let () = ignore (pattern_of_constr env ty) in
+        assert (not b); PMeta (Some id)
       | Evar_kinds.GoalEvar -> 
 	PEvar (evk,Array.map (pattern_of_constr env) ctxt)
       | _ -> 
@@ -189,12 +179,7 @@ let pattern_of_constr env sigma t =
 	       Array.to_list (Array.mapi branch_of_constr br))
     | 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 *)
-  (sigma,!ctx,p)
+  pattern_of_constr env t
 
 (* To process patterns, we need a translation without typing at all. *)
 
@@ -234,7 +219,7 @@ let instantiate_pattern env sigma lvar c =
               ctx
           in
 	  let c = substl inst c in
-	  pi3 (pattern_of_constr env sigma c)
+	  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
@@ -259,7 +244,7 @@ let rec subst_pattern subst pat =
   | PRef ref ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then pat else
-	 pi3 (pattern_of_constr (Global.env()) Evd.empty t)
+	 pattern_of_constr (Global.env()) Evd.empty t
   | PVar _
   | PEvar _
   | PRel _ -> pat
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 9e72280fe2..0148280287 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -39,8 +39,7 @@ 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 -> 
-  Evd.evar_map * named_context * constr_pattern
+val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> 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 5630d20b5d..6250886821 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -677,7 +677,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 = pi3 (Patternops.pattern_of_constr env sigma cty) in
+	let pat = Patternops.pattern_of_constr env sigma cty in
 	let hd =
 	  try head_pattern_bound pat
 	  with BoundPattern -> failwith "make_exact_entry"
@@ -696,7 +696,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 = pi3 (Patternops.pattern_of_constr env ce.evd c') in
+	let pat = Patternops.pattern_of_constr env ce.evd c' in
         let hd =
 	  try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry" in
@@ -794,7 +794,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 (pi3 (Patternops.pattern_of_constr env ce.evd (clenv_type ce)));
+              pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce));
 	      name = name;
               code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d244129425..ee21a51598 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -688,12 +688,12 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
       try Inl (coerce_to_evaluable_ref env x)
       with CannotCoerceTo _ ->
         let c = coerce_to_closed_constr env x in
-        Inr (pi3 (pattern_of_constr env sigma c)) in
+        Inr (pattern_of_constr env sigma c) in
     (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id)
      with Not_found ->
        error_global_not_found_loc loc (qualid_of_ident id))
   | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
-  | Inr c -> Inr (pi3 (interp_typed_pattern ist env sigma c)) in
+  | Inr c -> Inr (interp_typed_pattern ist env sigma c) in
   interp_occurrences ist occs, p
 
 let interp_constr_with_occurrences_and_name_as_list =
@@ -1043,7 +1043,7 @@ let use_types = false
 let eval_pattern lfun ist env sigma ((glob,_),pat as c) =
   let bound_names = bound_glob_vars glob in
   if use_types then
-    (bound_names,pi3 (interp_typed_pattern ist env sigma c))
+    (bound_names,interp_typed_pattern ist env sigma c)
   else
     (bound_names,instantiate_pattern env sigma lfun pat)
 
@@ -2154,7 +2154,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 (sigma,sign,op) = interp_typed_pattern ist env sigma op in
+          let op = interp_typed_pattern ist env sigma op in
           let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
           let c_interp patvars sigma =
 	    let lfun' = Id.Map.fold (fun id c lfun ->
@@ -2167,7 +2167,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
 		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 with sigma = sigma }
+	      gl
         end
       end
       end