rahmenlose Ansicht.mlg DruckansichtUnknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
(************************************************************************)
(* * 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) *)
(************************************************************************)
{
open Ltac_plugin
open Stdarg
open Tacarg
let locality = Zify.zify_register_locality
}
DECLARE PLUGIN "rocq-runtime.plugins.zify"
VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF
| #[ locality ] ["Add" "Zify" "InjTyp" reference(t) ] -> { Zify.InjTable.register locality t }
| #[ locality ] ["Add" "Zify" "BinOp" reference(t) ] -> { Zify.BinOp.register locality t }
| #[ locality ] ["Add" "Zify" "UnOp" reference(t) ] -> { Zify.UnOp.register locality t }
| #[ locality ] ["Add" "Zify" "CstOp" reference(t) ] -> { Zify.CstOp.register locality t }
| #[ locality ] ["Add" "Zify" "BinRel" reference(t) ] -> { Zify.BinRel.register locality t }
| #[ locality ] ["Add" "Zify" "PropOp" reference(t) ] -> { Zify.PropBinOp.register locality t }
| #[ locality ] ["Add" "Zify" "PropBinOp" reference(t) ] -> { Zify.PropBinOp.register locality t }
| #[ locality ] ["Add" "Zify" "PropUOp" reference(t) ] -> { Zify.PropUnOp.register locality t }
| #[ locality ] ["Add" "Zify" "BinOpSpec" reference(t) ] -> { Zify.BinOpSpec.register locality t }
| #[ locality ] ["Add" "Zify" "UnOpSpec" reference(t) ] -> { Zify.UnOpSpec.register locality t }
| #[ locality ] ["Add" "Zify" "Saturate" reference(t) ] -> { Zify.Saturate.register locality t }
END
TACTIC EXTEND ITER
| [ "zify_iter_specs"] -> { Zify.iter_specs}
END
TACTIC EXTEND TRANS
| [ "zify_op" ] -> { Zify.zify_tac }
| [ "zify_saturate" ] -> { Zify.saturate }
| [ "zify_iter_let" tactic(t)] -> { Zify.iter_let t }
| [ "zify_elim_let" ] -> { Zify.elim_let }
END
VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF
|[ "Show" "Zify" "InjTyp" ] -> { Zify.InjTable.print () }
|[ "Show" "Zify" "BinOp" ] -> { Zify.BinOp.print () }
|[ "Show" "Zify" "UnOp" ] -> { Zify.UnOp.print () }
|[ "Show" "Zify" "CstOp"] -> { Zify.CstOp.print () }
|[ "Show" "Zify" "BinRel"] -> { Zify.BinRel.print () }
|[ "Show" "Zify" "UnOpSpec"] -> { Zify.UnOpSpec.print() }
|[ "Show" "Zify" "BinOpSpec"] -> { Zify.BinOpSpec.print() }
END
[ Verzeichnis aufwärts0.67unsichere Verbindung
]
