blob: 74b070874370c720587930d1dd62dc22b95404c5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq 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 warn_deprecated_Spec =
CWarnings.create ~name:"deprecated-Zify-Spec" ~category:"deprecated"
(fun () ->
Pp.strbrk ("Show Zify Spec is deprecated. Use either \"Show Zify BinOpSpec\" or \"Show Zify UnOpSpec\"."))
}
DECLARE PLUGIN "zify_plugin"
VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF
| ["Add" "Zify" "InjTyp" constr(t) ] -> { Zify.InjTable.register t }
| ["Add" "Zify" "BinOp" constr(t) ] -> { Zify.BinOp.register t }
| ["Add" "Zify" "UnOp" constr(t) ] -> { Zify.UnOp.register t }
| ["Add" "Zify" "CstOp" constr(t) ] -> { Zify.CstOp.register t }
| ["Add" "Zify" "BinRel" constr(t) ] -> { Zify.BinRel.register t }
| ["Add" "Zify" "PropOp" constr(t) ] -> { Zify.PropBinOp.register t }
| ["Add" "Zify" "PropBinOp" constr(t) ] -> { Zify.PropBinOp.register t }
| ["Add" "Zify" "PropUOp" constr(t) ] -> { Zify.PropUnOp.register t }
| ["Add" "Zify" "BinOpSpec" constr(t) ] -> { Zify.BinOpSpec.register t }
| ["Add" "Zify" "UnOpSpec" constr(t) ] -> { Zify.UnOpSpec.register t }
| ["Add" "Zify" "Saturate" constr(t) ] -> { Zify.Saturate.register 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
|
