diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-19 17:48:32 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-19 17:52:26 +0100 |
| commit | 9d47cc0af706ed1cd4ab87c2d402a0457a9b6a5c (patch) | |
| tree | bf7c7746400e696d4fb3f2e7c677e955f8a52066 /pretyping/patternops.mli | |
| parent | 6ababf42b3f03926c30cfbd209436ec83a21769e (diff) | |
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.
Diffstat (limited to 'pretyping/patternops.mli')
| -rw-r--r-- | pretyping/patternops.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 9e72280fe..014828028 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 |