From 2d3916766d3f145643a994aa83174c98394d5baa Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 3 Mar 2015 21:45:42 +0100
Subject: 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.

---
 pretyping/patternops.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping/patternops.mli')

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
-- 
cgit v1.2.3