aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-02-28 15:30:15 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-04-10 17:19:21 +0200
commit306b45f889f83846b1ab10d3b37d9f3e7817a5db (patch)
tree0aaf21c4606927f7af784c38ab1da4b25fd9f542 /pretyping
parent834530272b9006e28a4b7ba35b1f8f861f51e7ce (diff)
Do not compute constr matching context if not used.
This mitigates bug #6860.
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/constr_matching.ml4
-rw-r--r--pretyping/constr_matching.mli2
2 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 89d490a41..b4e1a1b10 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -427,7 +427,7 @@ let special_meta = (-1)
type matching_result =
{ m_sub : bound_ident_map * patvar_map;
- m_ctx : constr; }
+ m_ctx : constr Lazy.t; }
let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) )
@@ -451,7 +451,7 @@ let authorized_occ env sigma closed pat c mk_ctx =
let subst = matches_core_closed env sigma pat c in
if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst)
then (fun next -> next ())
- else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next)
+ else (fun next -> mkresult subst (lazy (mk_ctx (mkMeta special_meta))) next)
with PatternMatchingFailure -> (fun next -> next ())
let subargs env v = Array.map_to_list (fun c -> (env, c)) v
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],