From 556c2ce6f1b09d09484cc83f6ada213496add45b Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 2 Jul 2013 17:28:22 +0000
Subject: Removing the use of leveled tactics wit_tacticn. It is now handled
 through a unique generic argument, and the level is only considered at
 parsing time.

This may introduce unnecessary parentheses in Ltac printing though,
as every tactic argument is collapsed at the lowest level. I assume
this does not matter that much, and anyway Ltac printing is quite
bugged as of today.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16616 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrarg.ml  | 8 +++++++-
 interp/constrarg.mli | 2 ++
 2 files changed, 9 insertions(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 87da56e4fc..5c2b3392c4 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -14,6 +14,7 @@ open Libnames
 open Globnames
 open Glob_term
 open Genredexpr
+open Tacexpr
 open Pattern
 open Constrexpr
 open Term
@@ -35,6 +36,9 @@ let wit_int_or_var = unsafe_of_type IntOrVarArgType
 let wit_intro_pattern : intro_pattern_expr located uniform_genarg_type =
   Genarg.make0 None "intropattern"
 
+let wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type =
+  Genarg.make0 None "tactic"
+
 let wit_ident_gen b = unsafe_of_type (IdentArgType b)
 
 let wit_ident = wit_ident_gen true
@@ -69,4 +73,6 @@ let wit_red_expr = unsafe_of_type RedExprArgType
 
 (** Register location *)
 
-let () = register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern"
+let () =
+  register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern";
+  register_name0 wit_tactic "Constrarg.wit_tactic"
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 548bd66905..1233e165fd 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -77,3 +77,5 @@ val wit_red_expr :
   ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
   (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
+
+val wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
-- 
cgit v1.2.3