diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-03-03 21:45:42 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-03-03 22:15:10 +0100 |
| commit | 2d3916766d3f145643a994aa83174c98394d5baa (patch) | |
| tree | a1e687c049a1ad11484ed41507c06b55ddb959e6 /pretyping/patternops.mli | |
| parent | 2f8a153dafb144b3fbf984680b4da7bc06c357c2 (diff) | |
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.
Diffstat (limited to 'pretyping/patternops.mli')
| -rw-r--r-- | pretyping/patternops.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index cf02421c2..9e72280fe 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 |