aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--plugins/btauto/g_btauto.mlg (renamed from plugins/btauto/g_btauto.ml4)6
-rw-r--r--plugins/cc/g_congruence.mlg (renamed from plugins/cc/g_congruence.ml4)14
-rw-r--r--plugins/fourier/g_fourier.mlg (renamed from plugins/fourier/g_fourier.ml4)6
-rw-r--r--plugins/ltac/coretactics.mlg (renamed from plugins/ltac/coretactics.ml4)182
-rw-r--r--plugins/ltac/g_eqdecide.mlg (renamed from plugins/ltac/g_eqdecide.ml4)8
-rw-r--r--plugins/micromega/g_micromega.mlg (renamed from plugins/micromega/g_micromega.ml4)38
-rw-r--r--plugins/nsatz/g_nsatz.mlg (renamed from plugins/nsatz/g_nsatz.ml4)6
-rw-r--r--plugins/omega/g_omega.mlg (renamed from plugins/omega/g_omega.ml4)9
-rw-r--r--plugins/quote/g_quote.mlg (renamed from plugins/quote/g_quote.ml4)16
-rw-r--r--plugins/romega/g_romega.mlg (renamed from plugins/romega/g_romega.ml4)12
-rw-r--r--plugins/rtauto/g_rtauto.mlg (renamed from plugins/rtauto/g_rtauto.ml4)5
11 files changed, 182 insertions, 120 deletions
diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.mlg
index 3ae0f45cb..312ef1e55 100644
--- a/plugins/btauto/g_btauto.ml4
+++ b/plugins/btauto/g_btauto.mlg
@@ -8,11 +8,15 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+{
+
open Ltac_plugin
+}
+
DECLARE PLUGIN "btauto_plugin"
TACTIC EXTEND btauto
-| [ "btauto" ] -> [ Refl_btauto.Btauto.tac ]
+| [ "btauto" ] -> { Refl_btauto.Btauto.tac }
END
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.mlg
index fb013ac13..685059294 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.mlg
@@ -8,22 +8,26 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+{
+
open Ltac_plugin
open Cctac
open Stdarg
+}
+
DECLARE PLUGIN "cc_plugin"
(* Tactic registration *)
TACTIC EXTEND cc
- [ "congruence" ] -> [ congruence_tac 1000 [] ]
- |[ "congruence" integer(n) ] -> [ congruence_tac n [] ]
- |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ]
+| [ "congruence" ] -> { congruence_tac 1000 [] }
+| [ "congruence" integer(n) ] -> { congruence_tac n [] }
+| [ "congruence" "with" ne_constr_list(l) ] -> { congruence_tac 1000 l }
|[ "congruence" integer(n) "with" ne_constr_list(l) ] ->
- [ congruence_tac n l ]
+ { congruence_tac n l }
END
TACTIC EXTEND f_equal
- [ "f_equal" ] -> [ f_equal ]
+| [ "f_equal" ] -> { f_equal }
END
diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.mlg
index 44560ac18..703e29f96 100644
--- a/plugins/fourier/g_fourier.ml4
+++ b/plugins/fourier/g_fourier.mlg
@@ -8,11 +8,15 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+{
+
open Ltac_plugin
open FourierR
+}
+
DECLARE PLUGIN "fourier_plugin"
TACTIC EXTEND fourier
- [ "fourierz" ] -> [ fourier () ]
+| [ "fourierz" ] -> { fourier () }
END
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.mlg
index 61525cb49..a7331223e 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.mlg
@@ -8,6 +8,8 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+{
+
open Util
open Locus
open Tactypes
@@ -18,147 +20,151 @@ open Tacarg
open Names
open Logic
+}
+
DECLARE PLUGIN "ltac_plugin"
(** Basic tactics *)
TACTIC EXTEND reflexivity
- [ "reflexivity" ] -> [ Tactics.intros_reflexivity ]
+| [ "reflexivity" ] -> { Tactics.intros_reflexivity }
END
TACTIC EXTEND exact
- [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ]
+| [ "exact" casted_constr(c) ] -> { Tactics.exact_no_check c }
END
TACTIC EXTEND assumption
- [ "assumption" ] -> [ Tactics.assumption ]
+| [ "assumption" ] -> { Tactics.assumption }
END
TACTIC EXTEND etransitivity
- [ "etransitivity" ] -> [ Tactics.intros_transitivity None ]
+| [ "etransitivity" ] -> { Tactics.intros_transitivity None }
END
TACTIC EXTEND cut
- [ "cut" constr(c) ] -> [ Tactics.cut c ]
+| [ "cut" constr(c) ] -> { Tactics.cut c }
END
TACTIC EXTEND exact_no_check
- [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ]
+| [ "exact_no_check" constr(c) ] -> { Tactics.exact_no_check c }
END
TACTIC EXTEND vm_cast_no_check
- [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check c ]
+| [ "vm_cast_no_check" constr(c) ] -> { Tactics.vm_cast_no_check c }
END
TACTIC EXTEND native_cast_no_check
- [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check c ]
+| [ "native_cast_no_check" constr(c) ] -> { Tactics.native_cast_no_check c }
END
TACTIC EXTEND casetype
- [ "casetype" constr(c) ] -> [ Tactics.case_type c ]
+| [ "casetype" constr(c) ] -> { Tactics.case_type c }
END
TACTIC EXTEND elimtype
- [ "elimtype" constr(c) ] -> [ Tactics.elim_type c ]
+| [ "elimtype" constr(c) ] -> { Tactics.elim_type c }
END
TACTIC EXTEND lapply
- [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply c ]
+| [ "lapply" constr(c) ] -> { Tactics.cut_and_apply c }
END
TACTIC EXTEND transitivity
- [ "transitivity" constr(c) ] -> [ Tactics.intros_transitivity (Some c) ]
+| [ "transitivity" constr(c) ] -> { Tactics.intros_transitivity (Some c) }
END
(** Left *)
TACTIC EXTEND left
- [ "left" ] -> [ Tactics.left_with_bindings false NoBindings ]
+| [ "left" ] -> { Tactics.left_with_bindings false NoBindings }
END
TACTIC EXTEND eleft
- [ "eleft" ] -> [ Tactics.left_with_bindings true NoBindings ]
+| [ "eleft" ] -> { Tactics.left_with_bindings true NoBindings }
END
TACTIC EXTEND left_with
- [ "left" "with" bindings(bl) ] -> [
+| [ "left" "with" bindings(bl) ] -> {
Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.left_with_bindings false bl)
- ]
+ }
END
TACTIC EXTEND eleft_with
- [ "eleft" "with" bindings(bl) ] -> [
+| [ "eleft" "with" bindings(bl) ] -> {
Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.left_with_bindings true bl)
- ]
+ }
END
(** Right *)
TACTIC EXTEND right
- [ "right" ] -> [ Tactics.right_with_bindings false NoBindings ]
+| [ "right" ] -> { Tactics.right_with_bindings false NoBindings }
END
TACTIC EXTEND eright
- [ "eright" ] -> [ Tactics.right_with_bindings true NoBindings ]
+| [ "eright" ] -> { Tactics.right_with_bindings true NoBindings }
END
TACTIC EXTEND right_with
- [ "right" "with" bindings(bl) ] -> [
+| [ "right" "with" bindings(bl) ] -> {
Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.right_with_bindings false bl)
- ]
+ }
END
TACTIC EXTEND eright_with
- [ "eright" "with" bindings(bl) ] -> [
+| [ "eright" "with" bindings(bl) ] -> {
Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.right_with_bindings true bl)
- ]
+ }
END
(** Constructor *)
TACTIC EXTEND constructor
- [ "constructor" ] -> [ Tactics.any_constructor false None ]
-| [ "constructor" int_or_var(i) ] -> [
+| [ "constructor" ] -> { Tactics.any_constructor false None }
+| [ "constructor" int_or_var(i) ] -> {
Tactics.constructor_tac false None i NoBindings
- ]
-| [ "constructor" int_or_var(i) "with" bindings(bl) ] -> [
+ }
+| [ "constructor" int_or_var(i) "with" bindings(bl) ] -> {
let tac bl = Tactics.constructor_tac false None i bl in
Tacticals.New.tclDELAYEDWITHHOLES false bl tac
- ]
+ }
END
TACTIC EXTEND econstructor
- [ "econstructor" ] -> [ Tactics.any_constructor true None ]
-| [ "econstructor" int_or_var(i) ] -> [
+| [ "econstructor" ] -> { Tactics.any_constructor true None }
+| [ "econstructor" int_or_var(i) ] -> {
Tactics.constructor_tac true None i NoBindings
- ]
-| [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> [
+ }
+| [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> {
let tac bl = Tactics.constructor_tac true None i bl in
Tacticals.New.tclDELAYEDWITHHOLES true bl tac
- ]
+ }
END
(** Specialize *)
TACTIC EXTEND specialize
- [ "specialize" constr_with_bindings(c) ] -> [
+| [ "specialize" constr_with_bindings(c) ] -> {
Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None)
- ]
-| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> [
+ }
+| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> {
Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat))
- ]
+ }
END
TACTIC EXTEND symmetry
- [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ]
+| [ "symmetry" ] -> { Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} }
END
TACTIC EXTEND symmetry_in
-| [ "symmetry" "in" in_clause(cl) ] -> [ Tactics.intros_symmetry cl ]
+| [ "symmetry" "in" in_clause(cl) ] -> { Tactics.intros_symmetry cl }
END
(** Split *)
+{
+
let rec delayed_list = function
| [] -> fun _ sigma -> (sigma, [])
| x :: l ->
@@ -167,147 +173,159 @@ let rec delayed_list = function
let (sigma, l) = delayed_list l env sigma in
(sigma, x :: l)
+}
+
TACTIC EXTEND split
- [ "split" ] -> [ Tactics.split_with_bindings false [NoBindings] ]
+| [ "split" ] -> { Tactics.split_with_bindings false [NoBindings] }
END
TACTIC EXTEND esplit
- [ "esplit" ] -> [ Tactics.split_with_bindings true [NoBindings] ]
+| [ "esplit" ] -> { Tactics.split_with_bindings true [NoBindings] }
END
TACTIC EXTEND split_with
- [ "split" "with" bindings(bl) ] -> [
+| [ "split" "with" bindings(bl) ] -> {
Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.split_with_bindings false [bl])
- ]
+ }
END
TACTIC EXTEND esplit_with
- [ "esplit" "with" bindings(bl) ] -> [
+| [ "esplit" "with" bindings(bl) ] -> {
Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.split_with_bindings true [bl])
- ]
+ }
END
TACTIC EXTEND exists
- [ "exists" ] -> [ Tactics.split_with_bindings false [NoBindings] ]
-| [ "exists" ne_bindings_list_sep(bll, ",") ] -> [
+| [ "exists" ] -> { Tactics.split_with_bindings false [NoBindings] }
+| [ "exists" ne_bindings_list_sep(bll, ",") ] -> {
Tacticals.New.tclDELAYEDWITHHOLES false (delayed_list bll) (fun bll -> Tactics.split_with_bindings false bll)
- ]
+ }
END
TACTIC EXTEND eexists
- [ "eexists" ] -> [ Tactics.split_with_bindings true [NoBindings] ]
-| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> [
+| [ "eexists" ] -> { Tactics.split_with_bindings true [NoBindings] }
+| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> {
Tacticals.New.tclDELAYEDWITHHOLES true (delayed_list bll) (fun bll -> Tactics.split_with_bindings true bll)
- ]
+ }
END
(** Intro *)
TACTIC EXTEND intros_until
- [ "intros" "until" quantified_hypothesis(h) ] -> [ Tactics.intros_until h ]
+| [ "intros" "until" quantified_hypothesis(h) ] -> { Tactics.intros_until h }
END
TACTIC EXTEND intro
-| [ "intro" ] -> [ Tactics.intro_move None MoveLast ]
-| [ "intro" ident(id) ] -> [ Tactics.intro_move (Some id) MoveLast ]
-| [ "intro" ident(id) "at" "top" ] -> [ Tactics.intro_move (Some id) MoveFirst ]
-| [ "intro" ident(id) "at" "bottom" ] -> [ Tactics.intro_move (Some id) MoveLast ]
-| [ "intro" ident(id) "after" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveAfter h) ]
-| [ "intro" ident(id) "before" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveBefore h) ]
-| [ "intro" "at" "top" ] -> [ Tactics.intro_move None MoveFirst ]
-| [ "intro" "at" "bottom" ] -> [ Tactics.intro_move None MoveLast ]
-| [ "intro" "after" hyp(h) ] -> [ Tactics.intro_move None (MoveAfter h) ]
-| [ "intro" "before" hyp(h) ] -> [ Tactics.intro_move None (MoveBefore h) ]
+| [ "intro" ] -> { Tactics.intro_move None MoveLast }
+| [ "intro" ident(id) ] -> { Tactics.intro_move (Some id) MoveLast }
+| [ "intro" ident(id) "at" "top" ] -> { Tactics.intro_move (Some id) MoveFirst }
+| [ "intro" ident(id) "at" "bottom" ] -> { Tactics.intro_move (Some id) MoveLast }
+| [ "intro" ident(id) "after" hyp(h) ] -> { Tactics.intro_move (Some id) (MoveAfter h) }
+| [ "intro" ident(id) "before" hyp(h) ] -> { Tactics.intro_move (Some id) (MoveBefore h) }
+| [ "intro" "at" "top" ] -> { Tactics.intro_move None MoveFirst }
+| [ "intro" "at" "bottom" ] -> { Tactics.intro_move None MoveLast }
+| [ "intro" "after" hyp(h) ] -> { Tactics.intro_move None (MoveAfter h) }
+| [ "intro" "before" hyp(h) ] -> { Tactics.intro_move None (MoveBefore h) }
END
(** Move *)
TACTIC EXTEND move
- [ "move" hyp(id) "at" "top" ] -> [ Tactics.move_hyp id MoveFirst ]
-| [ "move" hyp(id) "at" "bottom" ] -> [ Tactics.move_hyp id MoveLast ]
-| [ "move" hyp(id) "after" hyp(h) ] -> [ Tactics.move_hyp id (MoveAfter h) ]
-| [ "move" hyp(id) "before" hyp(h) ] -> [ Tactics.move_hyp id (MoveBefore h) ]
+| [ "move" hyp(id) "at" "top" ] -> { Tactics.move_hyp id MoveFirst }
+| [ "move" hyp(id) "at" "bottom" ] -> { Tactics.move_hyp id MoveLast }
+| [ "move" hyp(id) "after" hyp(h) ] -> { Tactics.move_hyp id (MoveAfter h) }
+| [ "move" hyp(id) "before" hyp(h) ] -> { Tactics.move_hyp id (MoveBefore h) }
END
(** Rename *)
TACTIC EXTEND rename
-| [ "rename" ne_rename_list_sep(ids, ",") ] -> [ Tactics.rename_hyp ids ]
+| [ "rename" ne_rename_list_sep(ids, ",") ] -> { Tactics.rename_hyp ids }
END
(** Revert *)
TACTIC EXTEND revert
- [ "revert" ne_hyp_list(hl) ] -> [ Tactics.revert hl ]
+| [ "revert" ne_hyp_list(hl) ] -> { Tactics.revert hl }
END
(** Simple induction / destruct *)
+{
+
let simple_induct h =
Tacticals.New.tclTHEN (Tactics.intros_until h)
(Tacticals.New.onLastHyp Tactics.simplest_elim)
+}
+
TACTIC EXTEND simple_induction
- [ "simple" "induction" quantified_hypothesis(h) ] -> [ simple_induct h ]
+| [ "simple" "induction" quantified_hypothesis(h) ] -> { simple_induct h }
END
+{
+
let simple_destruct h =
Tacticals.New.tclTHEN (Tactics.intros_until h)
(Tacticals.New.onLastHyp Tactics.simplest_case)
+}
+
TACTIC EXTEND simple_destruct
- [ "simple" "destruct" quantified_hypothesis(h) ] -> [ simple_destruct h ]
+| [ "simple" "destruct" quantified_hypothesis(h) ] -> { simple_destruct h }
END
(** Double induction *)
TACTIC EXTEND double_induction
- [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
- [ Elim.h_double_induction h1 h2 ]
+| [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
+ { Elim.h_double_induction h1 h2 }
END
(* Admit *)
TACTIC EXTEND admit
- [ "admit" ] -> [ Proofview.give_up ]
+|[ "admit" ] -> { Proofview.give_up }
END
(* Fix *)
TACTIC EXTEND fix
- [ "fix" ident(id) natural(n) ] -> [ Tactics.fix id n ]
+| [ "fix" ident(id) natural(n) ] -> { Tactics.fix id n }
END
(* Cofix *)
TACTIC EXTEND cofix
- [ "cofix" ident(id) ] -> [ Tactics.cofix id ]
+| [ "cofix" ident(id) ] -> { Tactics.cofix id }
END
(* Clear *)
TACTIC EXTEND clear
- [ "clear" hyp_list(ids) ] -> [
+| [ "clear" hyp_list(ids) ] -> {
if List.is_empty ids then Tactics.keep []
else Tactics.clear ids
- ]
-| [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ]
+ }
+| [ "clear" "-" ne_hyp_list(ids) ] -> { Tactics.keep ids }
END
(* Clearbody *)
TACTIC EXTEND clearbody
- [ "clearbody" ne_hyp_list(ids) ] -> [ Tactics.clear_body ids ]
+| [ "clearbody" ne_hyp_list(ids) ] -> { Tactics.clear_body ids }
END
(* Generalize dependent *)
TACTIC EXTEND generalize_dependent
- [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep c ]
+| [ "generalize" "dependent" constr(c) ] -> { Tactics.generalize_dep c }
END
(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
+{
+
open Tacexpr
let initial_atomic () =
@@ -364,3 +382,5 @@ let initial_tacticals () =
]
let () = Mltop.declare_cache_obj initial_tacticals "ltac_plugin"
+
+}
diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.mlg
index 2251a6620..e57afe3e3 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.mlg
@@ -14,15 +14,19 @@
(* by Eduardo Gimenez *)
(************************************************************************)
+{
+
open Eqdecide
open Stdarg
+}
+
DECLARE PLUGIN "ltac_plugin"
TACTIC EXTEND decide_equality
-| [ "decide" "equality" ] -> [ decideEqualityGoal ]
+| [ "decide" "equality" ] -> { decideEqualityGoal }
END
TACTIC EXTEND compare
-| [ "compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ]
+| [ "compare" constr(c1) constr(c2) ] -> { compare c1 c2 }
END
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.mlg
index 81140a46a..21f0414e9 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.mlg
@@ -16,70 +16,74 @@
(* *)
(************************************************************************)
+{
+
open Ltac_plugin
open Stdarg
open Tacarg
+}
+
DECLARE PLUGIN "micromega_plugin"
TACTIC EXTEND RED
-| [ "myred" ] -> [ Tactics.red_in_concl ]
+| [ "myred" ] -> { Tactics.red_in_concl }
END
TACTIC EXTEND PsatzZ
-| [ "psatz_Z" int_or_var(i) tactic(t) ] -> [ (Coq_micromega.psatz_Z i
+| [ "psatz_Z" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Z i
(Tacinterp.tactic_of_value ist t))
- ]
-| [ "psatz_Z" tactic(t)] -> [ (Coq_micromega.psatz_Z (-1)) (Tacinterp.tactic_of_value ist t) ]
+ }
+| [ "psatz_Z" tactic(t)] -> { (Coq_micromega.psatz_Z (-1)) (Tacinterp.tactic_of_value ist t) }
END
TACTIC EXTEND Lia
-[ "xlia" tactic(t) ] -> [ (Coq_micromega.xlia (Tacinterp.tactic_of_value ist t)) ]
+| [ "xlia" tactic(t) ] -> { (Coq_micromega.xlia (Tacinterp.tactic_of_value ist t)) }
END
TACTIC EXTEND Nia
-[ "xnlia" tactic(t) ] -> [ (Coq_micromega.xnlia (Tacinterp.tactic_of_value ist t)) ]
+| [ "xnlia" tactic(t) ] -> { (Coq_micromega.xnlia (Tacinterp.tactic_of_value ist t)) }
END
TACTIC EXTEND NRA
-[ "xnra" tactic(t) ] -> [ (Coq_micromega.nra (Tacinterp.tactic_of_value ist t))]
+| [ "xnra" tactic(t) ] -> { (Coq_micromega.nra (Tacinterp.tactic_of_value ist t))}
END
TACTIC EXTEND NQA
-[ "xnqa" tactic(t) ] -> [ (Coq_micromega.nqa (Tacinterp.tactic_of_value ist t))]
+| [ "xnqa" tactic(t) ] -> { (Coq_micromega.nqa (Tacinterp.tactic_of_value ist t))}
END
TACTIC EXTEND Sos_Z
-| [ "sos_Z" tactic(t) ] -> [ (Coq_micromega.sos_Z (Tacinterp.tactic_of_value ist t)) ]
+| [ "sos_Z" tactic(t) ] -> { (Coq_micromega.sos_Z (Tacinterp.tactic_of_value ist t)) }
END
TACTIC EXTEND Sos_Q
-| [ "sos_Q" tactic(t) ] -> [ (Coq_micromega.sos_Q (Tacinterp.tactic_of_value ist t)) ]
+| [ "sos_Q" tactic(t) ] -> { (Coq_micromega.sos_Q (Tacinterp.tactic_of_value ist t)) }
END
TACTIC EXTEND Sos_R
-| [ "sos_R" tactic(t) ] -> [ (Coq_micromega.sos_R (Tacinterp.tactic_of_value ist t)) ]
+| [ "sos_R" tactic(t) ] -> { (Coq_micromega.sos_R (Tacinterp.tactic_of_value ist t)) }
END
TACTIC EXTEND LRA_Q
-[ "lra_Q" tactic(t) ] -> [ (Coq_micromega.lra_Q (Tacinterp.tactic_of_value ist t)) ]
+| [ "lra_Q" tactic(t) ] -> { (Coq_micromega.lra_Q (Tacinterp.tactic_of_value ist t)) }
END
TACTIC EXTEND LRA_R
-[ "lra_R" tactic(t) ] -> [ (Coq_micromega.lra_R (Tacinterp.tactic_of_value ist t)) ]
+| [ "lra_R" tactic(t) ] -> { (Coq_micromega.lra_R (Tacinterp.tactic_of_value ist t)) }
END
TACTIC EXTEND PsatzR
-| [ "psatz_R" int_or_var(i) tactic(t) ] -> [ (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) ]
-| [ "psatz_R" tactic(t) ] -> [ (Coq_micromega.psatz_R (-1) (Tacinterp.tactic_of_value ist t)) ]
+| [ "psatz_R" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) }
+| [ "psatz_R" tactic(t) ] -> { (Coq_micromega.psatz_R (-1) (Tacinterp.tactic_of_value ist t)) }
END
TACTIC EXTEND PsatzQ
-| [ "psatz_Q" int_or_var(i) tactic(t) ] -> [ (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) ]
-| [ "psatz_Q" tactic(t) ] -> [ (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) ]
+| [ "psatz_Q" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) }
+| [ "psatz_Q" tactic(t) ] -> { (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) }
END
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.mlg
index 4ac49adb9..16ff512e8 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.mlg
@@ -8,11 +8,15 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+{
+
open Ltac_plugin
open Stdarg
+}
+
DECLARE PLUGIN "nsatz_plugin"
TACTIC EXTEND nsatz_compute
-| [ "nsatz_compute" constr(lt) ] -> [ Nsatz.nsatz_compute (EConstr.Unsafe.to_constr lt) ]
+| [ "nsatz_compute" constr(lt) ] -> { Nsatz.nsatz_compute (EConstr.Unsafe.to_constr lt) }
END
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.mlg
index 170b937c9..c3d063cff 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.mlg
@@ -18,6 +18,8 @@
DECLARE PLUGIN "omega_plugin"
+{
+
open Ltac_plugin
open Names
open Coq_omega
@@ -43,14 +45,15 @@ let omega_tactic l =
(Tacticals.New.tclREPEAT (Tacticals.New.tclTHENLIST tacs))
(omega_solver)
+}
TACTIC EXTEND omega
-| [ "omega" ] -> [ omega_tactic [] ]
+| [ "omega" ] -> { omega_tactic [] }
END
TACTIC EXTEND omega'
| [ "omega" "with" ne_ident_list(l) ] ->
- [ omega_tactic (List.map Names.Id.to_string l) ]
-| [ "omega" "with" "*" ] -> [ omega_tactic ["nat";"positive";"N";"Z"] ]
+ { omega_tactic (List.map Names.Id.to_string l) }
+| [ "omega" "with" "*" ] -> { omega_tactic ["nat";"positive";"N";"Z"] }
END
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.mlg
index 09209dc22..749903c3a 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.mlg
@@ -8,6 +8,8 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+{
+
open Ltac_plugin
open Names
open Tacexpr
@@ -16,8 +18,12 @@ open Quote
open Stdarg
open Tacarg
+}
+
DECLARE PLUGIN "quote_plugin"
+{
+
let cont = Id.of_string "cont"
let x = Id.of_string "x"
@@ -27,12 +33,14 @@ let make_cont (k : Val.t) (c : EConstr.t) =
let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in
Tacinterp.eval_tactic_ist ist (TacArg (Loc.tag tac))
+}
+
TACTIC EXTEND quote
- [ "quote" ident(f) ] -> [ quote f [] ]
-| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ]
+| [ "quote" ident(f) ] -> { quote f [] }
+| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> { quote f lc }
| [ "quote" ident(f) "in" constr(c) "using" tactic(k) ] ->
- [ gen_quote (make_cont k) c f [] ]
+ { gen_quote (make_cont k) c f [] }
| [ "quote" ident(f) "[" ne_ident_list(lc) "]"
"in" constr(c) "using" tactic(k) ] ->
- [ gen_quote (make_cont k) c f lc ]
+ { gen_quote (make_cont k) c f lc }
END
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.mlg
index 5b77d08de..c1ce30027 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.mlg
@@ -9,6 +9,8 @@
DECLARE PLUGIN "romega_plugin"
+{
+
open Ltac_plugin
open Names
open Refl_omega
@@ -39,13 +41,15 @@ let romega_tactic unsafe l =
(Tactics.intros)
(total_reflexive_omega_tactic unsafe))
+}
+
TACTIC EXTEND romega
-| [ "romega" ] -> [ romega_tactic false [] ]
-| [ "unsafe_romega" ] -> [ romega_tactic true [] ]
+| [ "romega" ] -> { romega_tactic false [] }
+| [ "unsafe_romega" ] -> { romega_tactic true [] }
END
TACTIC EXTEND romega'
| [ "romega" "with" ne_ident_list(l) ] ->
- [ romega_tactic false (List.map Names.Id.to_string l) ]
-| [ "romega" "with" "*" ] -> [ romega_tactic false ["nat";"positive";"N";"Z"] ]
+ { romega_tactic false (List.map Names.Id.to_string l) }
+| [ "romega" "with" "*" ] -> { romega_tactic false ["nat";"positive";"N";"Z"] }
END
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.mlg
index aa6757634..9c9fdcfa2 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.mlg
@@ -8,12 +8,15 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+{
open Ltac_plugin
+}
+
DECLARE PLUGIN "rtauto_plugin"
TACTIC EXTEND rtauto
- [ "rtauto" ] -> [ Proofview.V82.tactic (Refl_tauto.rtauto_tac) ]
+| [ "rtauto" ] -> { Proofview.V82.tactic (Refl_tauto.rtauto_tac) }
END