mise sous CVS d'Omega

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@380 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 26 insertions, 0 deletions

diff --git a/contrib/omega/OmegaSyntax.v b/contrib/omega/OmegaSyntax.v
new file mode 100644
index 0000000000..dccfc5e890
--- /dev/null
+++ b/contrib/omega/OmegaSyntax.v
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*                                                                        *)
+(* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
+(*                                                                        *)
+(* Pierre Crégut (CNET, Lannion, France)                                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+Grammar vernac vernac :=
+  omega_sett [ "Set" "Omega" "Time" "." ] -> [(OmegaFlag "+time")]
+| omega_sets [ "Set" "Omega" "System" "." ] -> [(OmegaFlag "+system")]
+| omega_seta [ "Set" "Omega" "Action" "." ] -> [(OmegaFlag "+action")]
+| omega_unst [ "Unset" "Omega" "Time" "." ] -> [(OmegaFlag "-time")]
+| omega_unss [ "Unset" "Omega" "System" "." ] -> [(OmegaFlag "-system")]
+| omega_unsa [ "Unset" "Omega" "Action" "." ] -> [(OmegaFlag "-action")]
+| omega_swit [ "Switch" "Omega" "Time" "." ] -> [(OmegaFlag "time")]
+| omega_swis [ "Switch" "Omega" "System" "." ] -> [(OmegaFlag "system")]
+| omega_swia [ "Switch" "Omega" "Action" "." ] -> [(OmegaFlag "action")]
+| omega_set  [ "Set" "Omega" stringarg($id) "." ] -> [(OmegaFlag $id)].
+
+
+Grammar tactic simple_tactic :=
+  omega [ "Omega" ] -> [(Omega)].
+
+Syntax tactic level 0:
+  omega [(Omega)] -> ["Omega"].