From 7e613daf7c71a4180725bddb40151c2b5a6348f4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 22 Apr 2016 12:02:30 +0200
Subject: When interpreting "match goal with ... end" in ltac, expand evars by
 need at matching time rather than eagerly at the beginning of the call to
 "match".

To be done for other constructs too, e.g. "match term with ... endp".
---
 ltac/tacinterp.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'ltac')

diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index e8dee7a001..b742bb328d 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1530,7 +1530,9 @@ and interp_match ist lz constr lmr =
 
 (* Interprets the Match Context expressions *)
 and interp_match_goal ist lz lr lmr =
-    Ftactic.nf_enter { enter = begin fun gl ->
+    Ftactic.enter { enter = begin fun gl ->
+      (* Because match_goal will lazily whd_evar when necessary *)
+      let gl = Proofview.Goal.assume gl in
       let sigma = project gl in
       let env = Proofview.Goal.env gl in
       let hyps = Proofview.Goal.hyps gl in
-- 
cgit v1.2.3