Source file ce_syntax.ml
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
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
let _ = Mltop.add_known_module "orthologic-coq.plugin"
# 4 "src/ce_syntax.mlg"
open Ltac_plugin
open Stdarg
let () = Tacentries.tactic_extend "orthologic-coq.plugin" "OLGet" ~level:0
[(Tacentries.TyML (Tacentries.TyIdent ("olget", Tacentries.TyArg (
Extend.TUentry (Genarg.get_arg_tag wit_constr),
Tacentries.TyArg (
Extend.TUentry (Genarg.get_arg_tag wit_ident),
Tacentries.TyNil))),
(fun e h ist ->
# 15 "src/ce_syntax.mlg"
Ce_api.ol_normal e h
)))]
let () = Tacentries.tactic_extend "orthologic-coq.plugin" "OLCert" ~level:0
[(Tacentries.TyML (Tacentries.TyIdent ("olcert", Tacentries.TyArg (
Extend.TUentry (Genarg.get_arg_tag wit_constr),
Tacentries.TyArg (
Extend.TUentry (Genarg.get_arg_tag wit_ident),
Tacentries.TyNil))),
(fun e h ist ->
# 22 "src/ce_syntax.mlg"
Ce_api.ol_cert_tactic e h
)))]
let () = Tacentries.tactic_extend "orthologic-coq.plugin" "OLCertGoal" ~level:0
[(Tacentries.TyML (Tacentries.TyIdent ("olcert_goal", Tacentries.TyArg (
Extend.TUentry (Genarg.get_arg_tag wit_clause),
Tacentries.TyNil)),
(fun cl ist ->
# 29 "src/ce_syntax.mlg"
Ce_api.ol_cert_goal_tactic cl
)))]
let () = Tacentries.tactic_extend "orthologic-coq.plugin" "OLNormCert" ~level:0
[(Tacentries.TyML (Tacentries.TyIdent ("ol_norm_cert", Tacentries.TyArg (
Extend.TUentry (Genarg.get_arg_tag wit_constr),
Tacentries.TyArg (
Extend.TUentry (Genarg.get_arg_tag wit_clause),
Tacentries.TyNil))),
(fun e cl ist ->
# 36 "src/ce_syntax.mlg"
Ce_api.ol_norm_cert_tactic e cl
)))]
let () = Tacentries.tactic_extend "orthologic-coq.plugin" "OLNormCertGoal" ~level:0
[(Tacentries.TyML (Tacentries.TyIdent ("ol_norm_cert_goal",
Tacentries.TyArg (Extend.TUentry (Genarg.get_arg_tag wit_clause),
Tacentries.TyNil)), (fun cl ist ->
# 43 "src/ce_syntax.mlg"
Ce_api.ol_norm_cert_goal_tactic cl
)))]
let () = Tacentries.tactic_extend "orthologic-coq.plugin" "DestructAtom" ~level:0
[(Tacentries.TyML (Tacentries.TyIdent ("destruct_atom", Tacentries.TyNil),
(fun ist ->
# 50 "src/ce_syntax.mlg"
Ce_api.destruct_atom ()
)))]
let () = Tacentries.tactic_extend "orthologic-coq.plugin" "OLTautoCert" ~level:0
[(Tacentries.TyML (Tacentries.TyIdent ("oltauto_cert", Tacentries.TyArg (
Extend.TUentry (Genarg.get_arg_tag wit_clause),
Tacentries.TyNil)),
(fun cl ist ->
# 57 "src/ce_syntax.mlg"
Ce_api.oltauto_cert cl
)))]