From cdaf8e2ed109bd117da2366a279fa575d7b6185a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 10 Dec 2015 19:14:19 +0100
Subject: Fixing a pat%constr bug. Thanks to Enrico for reporting.

---
 tactics/tacinterp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 693b382cac..59420e4e01 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -866,7 +866,7 @@ and interp_intro_pattern_action ist env sigma = function
       let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in
       sigma, IntroInjection l
   | IntroApplyOn (c,ipat) ->
-      let c = fun env sigma -> interp_constr ist env sigma c in
+      let c = fun env sigma -> interp_open_constr ist env sigma c in
       let sigma,ipat = interp_intro_pattern ist env sigma ipat in
       sigma, IntroApplyOn (c,ipat)
   | IntroWildcard | IntroRewrite _ as x -> sigma, x
-- 
cgit v1.2.3