diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-02-28 15:30:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-10 17:19:21 +0200 |
| commit | 306b45f889f83846b1ab10d3b37d9f3e7817a5db (patch) | |
| tree | 0aaf21c4606927f7af784c38ab1da4b25fd9f542 /pretyping/constr_matching.mli | |
| parent | 834530272b9006e28a4b7ba35b1f8f861f51e7ce (diff) | |
Do not compute constr matching context if not used.
This mitigates bug #6860.
Diffstat (limited to 'pretyping/constr_matching.mli')
| -rw-r--r-- | pretyping/constr_matching.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 3c2c73915..d19789ef4 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -61,7 +61,7 @@ val is_matching_head : env -> Evd.evar_map -> constr_pattern -> constr -> bool (whose hole is denoted here with [special_meta]) *) type matching_result = { m_sub : bound_ident_map * patvar_map; - m_ctx : EConstr.t } + m_ctx : EConstr.t Lazy.t } (** [match_subterm pat c] returns the substitution and the context corresponding to each **closed** subterm of [c] matching [pat], |