diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /plugins/micromega/g_micromega.ml4 | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'plugins/micromega/g_micromega.ml4')
-rw-r--r-- | plugins/micromega/g_micromega.ml4 | 76 |
1 files changed, 76 insertions, 0 deletions
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 new file mode 100644 index 00000000..f4d04e5d --- /dev/null +++ b/plugins/micromega/g_micromega.ml4 @@ -0,0 +1,76 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* *) +(* Micromega: A reflexive tactic using the Positivstellensatz *) +(* *) +(* Frédéric Besson (Irisa/Inria) 2006-2008 *) +(* *) +(************************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +(* $Id$ *) + +open Quote +open Ring +open Mutils +open Rawterm +open Util + +let out_arg = function + | ArgVar _ -> anomaly "Unevaluated or_var variable" + | ArgArg x -> x + +TACTIC EXTEND PsatzZ +| [ "psatz_Z" int_or_var(i) ] -> [ Coq_micromega.psatz_Z (out_arg i) ] +| [ "psatz_Z" ] -> [ Coq_micromega.psatz_Z (-1) ] +END + +TACTIC EXTEND ZOmicron +[ "xlia" ] -> [ Coq_micromega.xlia] +END + + +TACTIC EXTEND Sos_Z +| [ "sos_Z" ] -> [ Coq_micromega.sos_Z] + END + +TACTIC EXTEND Sos_Q +| [ "sos_Q" ] -> [ Coq_micromega.sos_Q] + END + +TACTIC EXTEND Sos_R +| [ "sos_R" ] -> [ Coq_micromega.sos_R] +END + + +TACTIC EXTEND Omicron +[ "psatzl_Z" ] -> [ Coq_micromega.psatzl_Z] +END + +TACTIC EXTEND QOmicron +[ "psatzl_Q" ] -> [ Coq_micromega.psatzl_Q] +END + + + +TACTIC EXTEND ROmicron +[ "psatzl_R" ] -> [ Coq_micromega.psatzl_R] +END + +TACTIC EXTEND RMicromega +| [ "psatz_R" int_or_var(i) ] -> [ Coq_micromega.psatz_R (out_arg i) ] +| [ "psatz_R" ] -> [ Coq_micromega.psatz_R (-1) ] +END + + +TACTIC EXTEND QMicromega +| [ "psatz_Q" int_or_var(i) ] -> [ Coq_micromega.psatz_Q (out_arg i) ] +| [ "psatz_Q" ] -> [ Coq_micromega.psatz_Q (-1) ] +END + |