From 975e7cd2ad032668c7df690c9bdaa8cdbb196569 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 15 Sep 2016 16:09:17 +0200
Subject: Moving Ltac-specific generic arguments to their own file in the ltac/
 folder.

---
 ltac/extraargs.ml4     |  1 +
 ltac/extratactics.ml4  |  1 +
 ltac/g_class.ml4       |  1 +
 ltac/g_ltac.ml4        |  5 +++--
 ltac/g_obligations.ml4 |  1 +
 ltac/ltac.mllib        |  1 +
 ltac/pltac.ml          |  1 +
 ltac/pptactic.ml       |  3 ++-
 ltac/tacarg.ml         | 26 ++++++++++++++++++++++++++
 ltac/tacarg.mli        | 27 +++++++++++++++++++++++++++
 ltac/tacentries.ml     | 10 +++++-----
 ltac/tacintern.ml      |  1 +
 ltac/tacinterp.ml      |  1 +
 ltac/tacsubst.ml       |  1 +
 14 files changed, 72 insertions(+), 8 deletions(-)
 create mode 100644 ltac/tacarg.ml
 create mode 100644 ltac/tacarg.mli

(limited to 'ltac')

diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index c32f757d9c..1176772cdc 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -12,6 +12,7 @@ open Pp
 open Genarg
 open Stdarg
 open Constrarg
+open Tacarg
 open Pcoq.Prim
 open Pcoq.Constr
 open Names
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index d16ed84a24..de701bb239 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -12,6 +12,7 @@ open Pp
 open Genarg
 open Stdarg
 open Constrarg
+open Tacarg
 open Extraargs
 open Pcoq.Prim
 open Pltac
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index 3cdb3a6c7d..b662057ba3 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -13,6 +13,7 @@ open Class_tactics
 open Pltac
 open Stdarg
 open Constrarg
+open Tacarg
 
 DECLARE PLUGIN "g_class"
 
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index f17cbc9a3b..cce0689107 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -34,7 +34,7 @@ let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) ()
 let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n
 let genarg_of_ipattern pat = in_gen (rawwit Constrarg.wit_intro_pattern) pat
 let genarg_of_uconstr c = in_gen (rawwit Constrarg.wit_uconstr) c
-let in_tac tac = in_gen (rawwit Constrarg.wit_ltac) tac
+let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac
 
 let reference_to_id = function
   | Libnames.Ident (loc, id) -> (loc, id)
@@ -348,12 +348,13 @@ GEXTEND Gram
   ;
   operconstr: LEVEL "0"
     [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
-          let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in
+          let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in
           CHole (!@loc, None, IntroAnonymous, Some arg) ] ]
   ;
   END
 
 open Constrarg
+open Tacarg
 open Vernacexpr
 open Vernac_classifier
 open Goptions
diff --git a/ltac/g_obligations.ml4 b/ltac/g_obligations.ml4
index df0b3e855e..fd531ca691 100644
--- a/ltac/g_obligations.ml4
+++ b/ltac/g_obligations.ml4
@@ -18,6 +18,7 @@ open Constrexpr
 open Constrexpr_ops
 open Stdarg
 open Constrarg
+open Tacarg
 open Extraargs
 
 let (set_default_tactic, get_default_tactic, print_default_tactic) = 
diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib
index b9b63be3aa..029dfd393f 100644
--- a/ltac/ltac.mllib
+++ b/ltac/ltac.mllib
@@ -1,3 +1,4 @@
+Tacarg
 Pptactic
 Pltac
 Taccoerce
diff --git a/ltac/pltac.ml b/ltac/pltac.ml
index 148867aacb..94bf32d1d5 100644
--- a/ltac/pltac.ml
+++ b/ltac/pltac.ml
@@ -50,6 +50,7 @@ let tactic_eoi = eoi_entry tactic
 let () =
   let open Stdarg in
   let open Constrarg in
+  let open Tacarg in
   register_grammar wit_int_or_var (int_or_var);
   register_grammar wit_intro_pattern (simple_intropattern);
   register_grammar wit_quant_hyp (quantified_hypothesis);
diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml
index a4222ae2ca..dc2676bf4b 100644
--- a/ltac/pptactic.ml
+++ b/ltac/pptactic.ml
@@ -16,6 +16,7 @@ open Tacexpr
 open Genarg
 open Geninterp
 open Constrarg
+open Tacarg
 open Libnames
 open Ppextend
 open Misctypes
@@ -1305,7 +1306,7 @@ let () =
     (pr_with_bindings pr_constr_expr pr_lconstr_expr)
     (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
     (fun it -> pr_with_bindings pr_constr pr_lconstr (fst (run_delayed it)));
-  Genprint.register_print0 Constrarg.wit_destruction_arg
+  Genprint.register_print0 Tacarg.wit_destruction_arg
     (pr_destruction_arg pr_constr_expr pr_lconstr_expr)
     (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
     (fun it -> pr_destruction_arg pr_constr pr_lconstr (run_delayed_destruction_arg it));
diff --git a/ltac/tacarg.ml b/ltac/tacarg.ml
new file mode 100644
index 0000000000..42552c4846
--- /dev/null
+++ b/ltac/tacarg.ml
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Generic arguments based on Ltac. *)
+
+open Genarg
+open Geninterp
+open Tacexpr
+
+let make0 ?dyn name =
+  let wit = Genarg.make0 name in
+  let () = Geninterp.register_val0 wit dyn in
+  wit
+
+let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
+  make0 "tactic"
+
+let wit_ltac = make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac"
+
+let wit_destruction_arg =
+  make0 "destruction_arg"
diff --git a/ltac/tacarg.mli b/ltac/tacarg.mli
new file mode 100644
index 0000000000..bfa423db20
--- /dev/null
+++ b/ltac/tacarg.mli
@@ -0,0 +1,27 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Genarg
+open Tacexpr
+open Constrexpr
+open Misctypes
+
+(** Generic arguments based on Ltac. *)
+
+val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_type
+
+(** [wit_ltac] is subtly different from [wit_tactic]: they only change for their
+    toplevel interpretation. The one of [wit_ltac] forces the tactic and
+    discards the result. *)
+val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type
+
+val wit_destruction_arg :
+  (constr_expr with_bindings Tacexpr.destruction_arg,
+   glob_constr_and_expr with_bindings Tacexpr.destruction_arg,
+   delayed_open_constr_with_bindings Tacexpr.destruction_arg) genarg_type
+
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index fcdb1875d0..2e2b55be74 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -56,9 +56,9 @@ let get_tacentry n m =
     && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
     && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
   in
-  if check_lvl n then EntryName (rawwit Constrarg.wit_tactic, Aself)
-  else if check_lvl (n + 1) then EntryName (rawwit Constrarg.wit_tactic, Anext)
-  else EntryName (rawwit Constrarg.wit_tactic, atactic n)
+  if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Aself)
+  else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Anext)
+  else EntryName (rawwit Tacarg.wit_tactic, atactic n)
 
 let get_separator = function
 | None -> error "Missing separator."
@@ -163,7 +163,7 @@ let add_tactic_entry (kn, ml, tg) state =
   let mkact loc l =
     let map arg =
       (** HACK to handle especially the tactic(...) entry *)
-      let wit = Genarg.rawwit Constrarg.wit_tactic in
+      let wit = Genarg.rawwit Tacarg.wit_tactic in
       if Genarg.has_type arg wit && not ml then
         Tacexp (Genarg.out_gen wit arg)
       else
@@ -218,7 +218,7 @@ let interp_prod_item = function
     | Some n ->
       (** FIXME: do better someday *)
       assert (String.equal s "tactic");
-      begin match Constrarg.wit_tactic with
+      begin match Tacarg.wit_tactic with
       | ExtraArg tag -> ArgT.Any tag
       | _ -> assert false
       end
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index b1de30893d..b0b4dc3579 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -24,6 +24,7 @@ open Termops
 open Tacexpr
 open Genarg
 open Constrarg
+open Tacarg
 open Misctypes
 open Locus
 
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 9e502682b8..a65e58ddb0 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -32,6 +32,7 @@ open Genarg
 open Geninterp
 open Stdarg
 open Constrarg
+open Tacarg
 open Printer
 open Pretyping
 open Misctypes
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index cce4382c2c..e0fdc4e5a1 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -11,6 +11,7 @@ open Tacexpr
 open Mod_subst
 open Genarg
 open Constrarg
+open Tacarg
 open Misctypes
 open Globnames
 open Term
-- 
cgit v1.2.3