From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- plugins/micromega/g_micromega.ml4 | 53 +++++++++++++++++++++------------------ 1 file changed, 29 insertions(+), 24 deletions(-) (limited to 'plugins/micromega/g_micromega.ml4') 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 -- cgit v1.2.3