Merge PR #7213: Do not compute constr matching context if not used.

2 files changed, 3 insertions, 3 deletions

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 89d490a410..b4e1a1b102 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 3c2c73915f..d19789ef42 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],