aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/argextend.ml47
-rw-r--r--grammar/q_util.ml415
-rw-r--r--interp/constrarg.ml10
-rw-r--r--interp/constrarg.mli12
-rw-r--r--interp/stdarg.ml5
-rw-r--r--interp/stdarg.mli5
-rw-r--r--plugins/cc/g_congruence.ml44
-rw-r--r--plugins/derive/g_derive.ml44
-rw-r--r--plugins/extraction/g_extraction.ml44
-rw-r--r--plugins/firstorder/g_ground.ml44
-rw-r--r--plugins/funind/g_indfun.ml44
-rw-r--r--plugins/micromega/g_micromega.ml44
-rw-r--r--plugins/omega/g_omega.ml42
-rw-r--r--plugins/quote/g_quote.ml44
-rw-r--r--plugins/romega/g_romega.ml42
-rw-r--r--plugins/setoid_ring/g_newring.ml45
-rw-r--r--tactics/coretactics.ml47
-rw-r--r--tactics/extraargs.ml44
-rw-r--r--tactics/extraargs.mli1
-rw-r--r--tactics/extratactics.ml47
-rw-r--r--tactics/g_auto.ml47
-rw-r--r--tactics/g_class.ml45
-rw-r--r--tactics/g_rewrite.ml45
-rw-r--r--toplevel/g_obligations.ml46
24 files changed, 110 insertions, 23 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 57ae357de..41e94914e 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -23,12 +23,7 @@ let qualified_name loc s =
let (name, path) = CList.sep_last path in
qualified_name loc path name
-let mk_extraarg loc s =
- try
- let name = Genarg.get_name0 s in
- qualified_name loc name
- with Not_found ->
- <:expr< $lid:"wit_"^s$ >>
+let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >>
let rec make_wit loc = function
| ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >>
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 1848bf85f..3946d5d2b 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -47,15 +47,6 @@ let mlexpr_of_option f = function
let mlexpr_of_ident id =
<:expr< Names.Id.of_string $str:id$ >>
-let repr_entry e =
- let entry u =
- let _ = Pcoq.get_entry u e in
- Some (Entry.univ_name u, e)
- in
- try entry Pcoq.uprim with Not_found ->
- try entry Pcoq.uconstr with Not_found ->
- try entry Pcoq.utactic with Not_found -> None
-
let rec mlexpr_of_prod_entry_key = function
| Extend.Ulist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >>
| Extend.Ulist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
@@ -63,11 +54,7 @@ let rec mlexpr_of_prod_entry_key = function
| Extend.Ulist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
| Extend.Uopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key s$ >>
| Extend.Umodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >>
- | Extend.Uentry e ->
- begin match repr_entry e with
- | None -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:e$) >>
- | Some (u, s) -> <:expr< Pcoq.Aentry (Entry.unsafe_of_name ($str:u$, $str:s$)) >>
- end
+ | Extend.Uentry e -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:e$) >>
| Extend.Uentryl (e, l) ->
(** Keep in sync with Pcoq! *)
assert (CString.equal e "tactic");
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index ead4e3969..20ee7aa4f 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -82,3 +82,13 @@ let () =
register_name0 wit_quant_hyp "Constrarg.wit_quant_hyp";
register_name0 wit_bindings "Constrarg.wit_bindings";
register_name0 wit_constr_with_bindings "Constrarg.wit_constr_with_bindings";
+ ()
+
+(** Aliases *)
+
+let wit_reference = wit_ref
+let wit_global = wit_ref
+let wit_clause = wit_clause_dft_concl
+let wit_quantified_hypothesis = wit_quant_hyp
+let wit_intropattern = wit_intro_pattern
+let wit_redexpr = wit_red_expr
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 5c26af3c2..1197b85a2 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -72,3 +72,15 @@ val wit_red_expr :
val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type
val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
+
+(** Aliases for compatibility *)
+
+val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type
+val wit_global : (reference, global_reference located or_var, global_reference) genarg_type
+val wit_clause : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
+val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
+val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
+val wit_redexpr :
+ ((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
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 56b995e53..e497c996f 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -28,3 +28,8 @@ let () = register_name0 wit_bool "Stdarg.wit_bool"
let () = register_name0 wit_int "Stdarg.wit_int"
let () = register_name0 wit_string "Stdarg.wit_string"
let () = register_name0 wit_pre_ident "Stdarg.wit_pre_ident"
+
+(** Aliases for compatibility *)
+
+let wit_integer = wit_int
+let wit_preident = wit_pre_ident
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index d8904dab8..e1f648d7f 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -19,3 +19,8 @@ val wit_int : int uniform_genarg_type
val wit_string : string uniform_genarg_type
val wit_pre_ident : string uniform_genarg_type
+
+(** Aliases for compatibility *)
+
+val wit_integer : int uniform_genarg_type
+val wit_preident : string uniform_genarg_type
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index 5dbc340ca..9a53e2e16 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -9,6 +9,10 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
open Cctac
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
DECLARE PLUGIN "cc_plugin"
diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4
index 18570a684..35a5a7616 100644
--- a/plugins/derive/g_derive.ml4
+++ b/plugins/derive/g_derive.ml4
@@ -6,6 +6,10 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+
(*i camlp4deps: "grammar/grammar.cma" i*)
let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater)
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index aec958689..7bd07f625 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -11,6 +11,10 @@
(* ML names *)
open Genarg
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
open Pp
open Names
open Nameops
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 3e8be3699..587d10d1c 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -15,6 +15,10 @@ open Goptions
open Tacticals
open Tacinterp
open Libnames
+open Constrarg
+open Stdarg
+open Pcoq.Prim
+open Pcoq.Tactic
DECLARE PLUGIN "ground_plugin"
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index dbcdeb83a..4bd69b9fe 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -16,8 +16,12 @@ open Constrexpr
open Indfun_common
open Indfun
open Genarg
+open Constrarg
open Tacticals
open Misctypes
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
DECLARE PLUGIN "recdef_plugin"
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index bfc9c727d..bca1c2feb 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -18,6 +18,10 @@
open Errors
open Misctypes
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Tactic
DECLARE PLUGIN "micromega_plugin"
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 04c62eb48..b314e0d85 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -19,6 +19,8 @@ DECLARE PLUGIN "omega_plugin"
open Names
open Coq_omega
+open Constrarg
+open Pcoq.Prim
let eval_tactic name =
let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 7a3d7936a..a15b0eb05 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -13,6 +13,10 @@ open Misctypes
open Tacexpr
open Geninterp
open Quote
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
DECLARE PLUGIN "quote_plugin"
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 6b2b2bbfa..61efa9f54 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -12,6 +12,8 @@ DECLARE PLUGIN "romega_plugin"
open Names
open Refl_omega
+open Constrarg
+open Pcoq.Prim
let eval_tactic name =
let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 856ec0db5..cd1d704dd 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -14,6 +14,11 @@ open Libnames
open Printer
open Newring_ast
open Newring
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
DECLARE PLUGIN "newring_plugin"
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 7da6df717..73b7bde9d 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -13,6 +13,11 @@ open Names
open Locus
open Misctypes
open Genredexpr
+open Stdarg
+open Constrarg
+open Pcoq.Constr
+open Pcoq.Prim
+open Pcoq.Tactic
open Proofview.Notations
open Sigma.Notations
@@ -143,7 +148,7 @@ END
TACTIC EXTEND symmetry
[ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ]
-| [ "symmetry" clause(cl) ] -> [ Tactics.intros_symmetry cl ]
+| [ "symmetry" clause_dft_concl(cl) ] -> [ Tactics.intros_symmetry cl ]
END
(** Split *)
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 98868e8f9..8215e785a 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -10,6 +10,10 @@
open Pp
open Genarg
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
open Names
open Tacexpr
open Taccoerce
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 7df845e4b..f7b379e69 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -53,7 +53,6 @@ val pr_by_arg_tac :
(int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->
raw_tactic_expr option -> Pp.std_ppcmds
-
(** Spiwack: Primitive for retroknowledge registration *)
val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ae8b83b95..52419497d 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -10,7 +10,12 @@
open Pp
open Genarg
+open Stdarg
+open Constrarg
open Extraargs
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
open Mod_subst
open Names
open Tacexpr
@@ -49,6 +54,8 @@ let replace_in_clause_maybe_by ist c1 c2 cl tac =
let replace_term ist dir_opt c cl =
with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl)
+let clause = Pcoq.Tactic.clause_dft_concl
+
TACTIC EXTEND replace
["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
-> [ replace_in_clause_maybe_by ist c1 c2 cl tac ]
diff --git a/tactics/g_auto.ml4 b/tactics/g_auto.ml4
index f4fae763f..788443944 100644
--- a/tactics/g_auto.ml4
+++ b/tactics/g_auto.ml4
@@ -10,6 +10,11 @@
open Pp
open Genarg
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
open Tacexpr
DECLARE PLUGIN "g_auto"
@@ -128,7 +133,7 @@ TACTIC EXTEND dfs_eauto
END
TACTIC EXTEND autounfold
-| [ "autounfold" hintbases(db) clause(cl) ] -> [ Eauto.autounfold_tac db cl ]
+| [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> [ Eauto.autounfold_tac db cl ]
END
TACTIC EXTEND autounfold_one
diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4
index 766593543..9ef154541 100644
--- a/tactics/g_class.ml4
+++ b/tactics/g_class.ml4
@@ -10,6 +10,11 @@
open Misctypes
open Class_tactics
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
+open Stdarg
+open Constrarg
DECLARE PLUGIN "g_class"
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index 0ce886373..c4ef1f297 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -20,6 +20,11 @@ open Extraargs
open Tacmach
open Tacticals
open Rewrite
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
DECLARE PLUGIN "g_rewrite"
diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4
index 2a5676525..dd11efebd 100644
--- a/toplevel/g_obligations.ml4
+++ b/toplevel/g_obligations.ml4
@@ -16,6 +16,12 @@
open Libnames
open Constrexpr
open Constrexpr_ops
+open Stdarg
+open Constrarg
+open Extraargs
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
(* We define new entries for programs, with the use of this module
* Subtac. These entries are named Subtac.<foo>
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-27 01:57:28 +0000