Merge PR #7979: TACTIC EXTEND in coqpp

1 files changed, 21 insertions, 17 deletions

diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.mlg
index 81140a46a9..21f0414e9c 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