diff options
Diffstat (limited to 'plugins/micromega/g_micromega.ml4')
| -rw-r--r-- | plugins/micromega/g_micromega.ml4 | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 23ae3bd0e..f4d04e5d4 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -31,6 +31,11 @@ TACTIC EXTEND PsatzZ | [ "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 @@ -53,9 +58,6 @@ TACTIC EXTEND QOmicron END -TACTIC EXTEND ZOmicron -[ "xlia" ] -> [ Coq_micromega.xlia] -END TACTIC EXTEND ROmicron [ "psatzl_R" ] -> [ Coq_micromega.psatzl_R] |