Quelle  g_micromega.mlg   Sprache: unbekannt

(************************************************************************)
(*         *      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           *)
(*                                                                      *)
(* * Mappings from Rocq tactics to Caml function calls                  *)
(*                                                                      *)
(*  Frédéric Besson (Irisa/Inria) 2006-2008                       *)
(*                                                                      *)
(************************************************************************)

{

open Ltac_plugin
open Stdarg
open Tacarg

}

DECLARE PLUGIN "rocq-runtime.plugins.micromega"

TACTIC EXTEND Lra_Q
| [ "xlra_Q"  tactic(t) ] -> { Coq_micromega.xlra_Q (Tacinterp.tactic_of_value ist t) }
END

TACTIC EXTEND Lra_wit_Q
| [ "wlra_Q" ident(w) constr(t) ] -> { Coq_micromega.wlra_Q w t }
END

TACTIC EXTEND Lra_R
| [ "xlra_R" tactic(t) ] -> { Coq_micromega.xlra_R (Tacinterp.tactic_of_value ist t) }
END

TACTIC EXTEND Lia
| [ "xlia" tactic(t) ] -> { Coq_micromega.xlia (Tacinterp.tactic_of_value ist t) }
END

TACTIC EXTEND Lia_wit
| [ "wlia" ident(w) constr(t) ] -> { Coq_micromega.wlia w t }
END

TACTIC EXTEND Nra_Q
| [ "xnra_Q" tactic(t) ] -> { Coq_micromega.xnra_Q (Tacinterp.tactic_of_value ist t) }
END

TACTIC EXTEND Nra_wit_Q
| [ "wnra_Q" ident(w) constr(t) ] -> { Coq_micromega.wnra_Q w t }
END

TACTIC EXTEND Nra_R
| [ "xnra_R" tactic(t) ] -> { Coq_micromega.xnra_R (Tacinterp.tactic_of_value ist t) }
END

TACTIC EXTEND Nia
| [ "xnia" tactic(t) ] -> { Coq_micromega.xnia (Tacinterp.tactic_of_value ist t) }
END

TACTIC EXTEND Nia_wit
| [ "wnia" ident(w) constr(t) ] -> { Coq_micromega.wnia w t }
END

TACTIC EXTEND Sos_Z
| [ "xsos_Z" tactic(t) ] -> { Coq_micromega.xsos_Z (Tacinterp.tactic_of_value ist t) }
END

TACTIC EXTEND Sos_wit_Z
| [ "wsos_Z" ident(w) constr(t) ] -> { Coq_micromega.wsos_Z w t }
END

TACTIC EXTEND Sos_Q
| [ "xsos_Q" tactic(t) ] -> { Coq_micromega.xsos_Q (Tacinterp.tactic_of_value ist t) }
END

TACTIC EXTEND Sos_wit_Q
| [ "wsos_Q" ident(w) constr(t) ] -> { Coq_micromega.wsos_Q w t }
END

TACTIC EXTEND Sos_R
| [ "xsos_R" tactic(t) ] -> { Coq_micromega.xsos_R (Tacinterp.tactic_of_value ist t) }
END

TACTIC EXTEND Psatz_Z
| [ "xpsatz_Z" nat_or_var(i) tactic(t) ] ->
  { Coq_micromega.xpsatz_Z i (Tacinterp.tactic_of_value ist t) }
END

TACTIC EXTEND Psatz_wit_Z
| [ "wpsatz_Z" nat_or_var(i) ident(w) constr(t) ] -> { Coq_micromega.wpsatz_Z i w t }
END

TACTIC EXTEND Psatz_Q
| [ "xpsatz_Q" nat_or_var(i) tactic(t) ] ->
  { Coq_micromega.xpsatz_Q i (Tacinterp.tactic_of_value ist t) }
END

TACTIC EXTEND Psatz_wit_Q
| [ "wpsatz_Q" nat_or_var(i) ident(w) constr(t) ] -> { Coq_micromega.wpsatz_Q i w t }
END

TACTIC EXTEND Psatz_R
| [ "xpsatz_R" nat_or_var(i) tactic(t) ] ->
  { Coq_micromega.xpsatz_R i (Tacinterp.tactic_of_value ist t) }
END

VERNAC COMMAND EXTEND ShowLiaProfile CLASSIFIED AS QUERY
| [ "Show" "Lia" "Profile" ] -> { Coq_micromega.print_lia_profile () }
END