1 files changed, 29 insertions, 24 deletions

diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 75237aaa..027f690f 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -16,63 +16,68 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open Errors
-open Misctypes
+open Constrarg
 
 DECLARE PLUGIN "micromega_plugin"
 
-let out_arg = function
-  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
-  | ArgArg x -> x
+TACTIC EXTEND RED
+| [ "myred"  ] -> [ Tactics.red_in_concl ]
+END
+
+
 
 TACTIC EXTEND PsatzZ
-| [ "psatz_Z" int_or_var(i) ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Z (out_arg i)) ]
-| [ "psatz_Z" ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Z (-1)) ]
+| [ "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) ]
 END
 
 TACTIC EXTEND Lia
-[ "xlia"  ] -> [  Proofview.V82.tactic (Coq_micromega.xlia) ]
+[ "xlia" tactic(t) ] -> [   (Coq_micromega.xlia (Tacinterp.tactic_of_value ist t)) ]
 END
 
 TACTIC EXTEND Nia
-[ "xnlia"  ] -> [  Proofview.V82.tactic (Coq_micromega.xnlia) ]
+[ "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))]
 END
 
+TACTIC EXTEND NQA
+[ "xnqa" tactic(t) ] -> [  (Coq_micromega.nqa (Tacinterp.tactic_of_value ist t))]
+END
 
 
+  
 TACTIC EXTEND Sos_Z
-| [ "sos_Z" ] -> [  Proofview.V82.tactic (Coq_micromega.sos_Z) ]
+| [ "sos_Z" tactic(t) ] -> [ (Coq_micromega.sos_Z (Tacinterp.tactic_of_value ist t)) ]
    END
 
 TACTIC EXTEND Sos_Q
-| [ "sos_Q" ] -> [  Proofview.V82.tactic (Coq_micromega.sos_Q) ]
+| [ "sos_Q" tactic(t) ] -> [   (Coq_micromega.sos_Q (Tacinterp.tactic_of_value ist t)) ]
    END
 
 TACTIC EXTEND Sos_R
-| [ "sos_R" ] -> [  Proofview.V82.tactic (Coq_micromega.sos_R) ]
-END
-
-(*
-TACTIC EXTEND Omicron
-[ "psatzl_Z"  ] -> [  Proofview.V82.tactic (Coq_micromega.psatzl_Z) ]
+| [ "sos_R" tactic(t) ] -> [   (Coq_micromega.sos_R (Tacinterp.tactic_of_value ist t)) ]
 END
-*)
 
 TACTIC EXTEND LRA_Q
-[ "psatzl_Q"  ] -> [  Proofview.V82.tactic (Coq_micromega.psatzl_Q) ]
+[ "lra_Q"  tactic(t) ] -> [   (Coq_micromega.lra_Q (Tacinterp.tactic_of_value ist t)) ]
 END
 
 TACTIC EXTEND LRA_R
-[ "psatzl_R"  ] -> [  Proofview.V82.tactic (Coq_micromega.psatzl_R) ]
+[ "lra_R" tactic(t) ] -> [   (Coq_micromega.lra_R (Tacinterp.tactic_of_value ist t)) ]
 END
 
 TACTIC EXTEND PsatzR
-| [ "psatz_R" int_or_var(i) ] -> [  Proofview.V82.tactic (Coq_micromega.psatz_R (out_arg i)) ]
-| [ "psatz_R" ] -> [  Proofview.V82.tactic (Coq_micromega.psatz_R (-1)) ]
+| [ "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) ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Q (out_arg i)) ]
-| [ "psatz_Q" ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Q (-1)) ]
+| [ "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