From 306b45f889f83846b1ab10d3b37d9f3e7817a5db Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 28 Feb 2018 15:30:15 +0100
Subject: Do not compute constr matching context if not used.

This mitigates bug #6860.
---
 pretyping/constr_matching.ml  | 4 ++--
 pretyping/constr_matching.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping')

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],
-- 
cgit v1.2.3