diff options
| author | Maxime Dénès | 2019-04-05 10:02:18 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-10 15:41:44 +0200 |
| commit | 61d53a17c594de1ea37b37f6215319d996ec31ea (patch) | |
| tree | 83c55ef28fd53d6f8af965e0c87ee6a168f90bb4 /pretyping/patternops.mli | |
| parent | 69c31d24fc8d058070cc7cadc1df28bfac7f6497 (diff) | |
Remove calls to Global.env in Patternops
Diffstat (limited to 'pretyping/patternops.mli')
| -rw-r--r-- | pretyping/patternops.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 90a536e780..3821fbf1a0 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -21,7 +21,7 @@ val constr_pattern_eq : constr_pattern -> constr_pattern -> bool val occur_meta_pattern : constr_pattern -> bool -val subst_pattern : Environ.env -> substitution -> constr_pattern -> constr_pattern +val subst_pattern : Environ.env -> Evd.evar_map -> substitution -> constr_pattern -> constr_pattern val noccurn_pattern : int -> constr_pattern -> bool |