Prepare move of micromega_tactics.v to Corelib

Author: proux01

theories/micromega/Lia.v

@@ -17,8 +17,7 @@
 From Stdlib Require Import PreOmega ZMicromega RingMicromega VarMap DeclConstantZ.
 From Stdlib Require Import BinNums.
 From Stdlib.micromega Require Tauto.
-Declare ML Module "rocq-runtime.plugins.micromega_core".
-Declare ML Module "rocq-runtime.plugins.micromega".
+From Stdlib Require Export micromega_tactics.
 
 Ltac zchecker :=
   let __wit := fresh "__wit" in

theories/micromega/Lqa.v

@@ -20,8 +20,7 @@ From Stdlib Require Import RingMicromega.
 From Stdlib Require Import VarMap.
 From Stdlib Require Import DeclConstant.
 From Stdlib.micromega Require Tauto.
-Declare ML Module "rocq-runtime.plugins.micromega_core".
-Declare ML Module "rocq-runtime.plugins.micromega".
+From Stdlib Require Export micromega_tactics.
 
 Ltac rchange :=
   let __wit := fresh "__wit" in

theories/micromega/Lra.v

@@ -21,8 +21,7 @@ From Stdlib Require Import RingMicromega.
 From Stdlib Require Import VarMap.
 From Stdlib.micromega Require Tauto.
 From Stdlib Require Import Rregisternames.
-
-Declare ML Module "rocq-runtime.plugins.micromega".
+From Stdlib Require Export micromega_tactics.
 
 Ltac rchange :=
   let __wit := fresh "__wit" in

theories/micromega/Psatz.v

@@ -26,8 +26,7 @@ From Stdlib.micromega Require Tauto.
 From Stdlib Require Lia.
 From Stdlib Require Lra.
 From Stdlib Require Lqa.
-
-Declare ML Module "rocq-runtime.plugins.micromega".
+From Stdlib Require Export micromega_tactics.
 
 Ltac lia := Lia.lia.
 

theories/micromega/micromega_tactics.v

@@ -0,0 +1,48 @@
+(************************************************************************)
+(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+(*                                                                      *)
+(* Micromega: A reflexive tactic using the Positivstellensatz           *)
+(*                                                                      *)
+(*  Frédéric Besson (Irisa/Inria)                                       *)
+(*                                                                      *)
+(************************************************************************)
+
+(* TODO: remove this file when requiring Rocq >= 9.2
+   and use the identical file in Corelib instead *)
+
+From Stdlib Require Import BinNums RatDef micromega_formula micromega_witness.
+
+(** This file provide access to the witness generation tactics
+of the micromega OCaml plugin. The following tactics are provided,
+where [ff : BFormula (Formula Q) isProp]:
+- wlra_Q wit ff : set [wit] to a value of type [Psatz Q]
+- wlia wit ff : set [wit] to a value of type [ZArithProof]
+- wnia wit ff : set [wit] to a value of type [ZArithProof]
+- wnra_Q wit ff : set [wit] to a value of type [Psatz Q]
+- wsos_Q wit ff : set [wit] to a value of type [Psatz Q]
+- wsos_Z wit ff : set [wit] to a value of type [Psatz Z]
+- wpsatz_Z <n> wit ff : set [wit] to a value of type [ZArithProof]
+- wpsatz_Q <n> wit ff : set [wit] to a value of type [Psatz Q]
+The last four require the external Csdp numerical solver.
+
+Beware that all tactic expect an Ltac name for [wit] and an actual
+value for [ff] (not just an identifier). That is, the following works
+<<
+  pose (ff := ...).
+  let ff' := eval unfold ff in ff in wlra_Q wit ff'.
+>>
+but not
+<<
+  pose (ff := ...).
+  wlra_Q wit ff.
+>>
+See test-suite/micromega/witness_tactics.v for an example. *)
+
+Declare ML Module "rocq-runtime.plugins.micromega".