From d288152f7d886ca6dba3944d20c6ca21452533da Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 20 Mar 2012 13:59:03 +0000
Subject: Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic
 tactic arguments of ltac functions).

Added support for recursive entries in ARGUMENT EXTEND, for right-hand
sides of ARGUMENT EXTEND raising exceptions and for right-hand sides
referring to "loc". Also fixed parsing level of initial value in
create_arg (raw instead of glob). Thanks to the Ssreflect plugin for
revealing these problems.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15065 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml  | 4 ++++
 tactics/tacinterp.mli | 2 ++
 2 files changed, 6 insertions(+)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a1e8f9bd1d..9da816d908 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2487,6 +2487,10 @@ let make_empty_glob_sign () =
   { ltacvars = ([],[]); ltacrecvars = [];
     gsigma = Evd.empty; genv = Global.env() }
 
+let fully_empty_glob_sign =
+  { ltacvars = ([],[]); ltacrecvars = [];
+    gsigma = Evd.empty; genv = Environ.empty_env }
+
 (* Initial call for interpretation *)
 let interp_tac_gen lfun avoid_ids debug t gl =
   interp_tactic { lfun=lfun; avoid_ids=avoid_ids; debug=debug; trace=[] }
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 4d01e5ad97..eff48b1004 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -78,6 +78,8 @@ type glob_sign = {
   gsigma : Evd.evar_map;
   genv : Environ.env }
 
+val fully_empty_glob_sign : glob_sign
+
 val add_interp_genarg :
   string ->
     (glob_sign -> raw_generic_argument -> glob_generic_argument) *
-- 
cgit v1.2.3