From 619b04a80ac6b17d54ac9227cba2d597cbda00a9 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 25 Nov 2013 11:41:27 +0100
Subject: Tacinterp: fewer use of old-style goals.

There are many functions in Tacinterp which use a goal as a proxy for the pair of an environment and an evar_map. But do not build LCF tactics with them. They don't play well with the new style of tactics.

I've changed some of them to explicitely take an environment and an evar_map instead.
---
 grammar/argextend.ml4 | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'grammar')

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 128b13bdae..d884a10cbb 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -170,7 +170,8 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
       | _ ->
 	<:expr< fun ist gl x ->
 	  let (sigma,a_interp) =
-	    Tacinterp.interp_genarg ist gl
+	    Tacinterp.interp_genarg ist
+              (Tacmach.pf_env gl) (Tacmach.project gl) (Tacmach.pf_concl gl) gl.Evd.it
                (Genarg.in_gen $make_globwit loc globtyp$ x)
 	  in
           (sigma , out_gen $make_topwit loc globtyp$ a_interp)>>
-- 
cgit v1.2.3