package orthologic-coq

You can search for identifiers within the package.

in-package search v0.2.0

A plugin to add orthologic-based tactics to Coq

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (1)

Authors

Maintainers

S

Simon Guilloud

Sources

orthologic-coq-0.9.1.tbz

sha256=60a9eeb27b6ad0a6fadb4127f5a7fdc194133dc55fa627e5eaedbee58a58651e

sha512=bab767857cecbb1529e599785f2485e62171a55b7ec34483976a9a15e8223167c52a2977f88752e64f17fd1b4e6fde682b608bd046b2a7867da2eca10844cf57

doc/src/orthologic-coq.plugin/ce_syntax.ml.html

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 Pp*)
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
  
           )))]

package orthologic-coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/src/orthologic-coq.plugin/ce_syntax.ml.html

Source file ce_syntax.ml

Source file `ce_syntax.ml`