package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

T

The Coq development team, INRIA, CNRS, and contributors.

Maintainers

C

coqdev@inria.fr

Sources

coq-8.15.0.tar.gz

sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3

doc/src/tuto0_plugin/g_tuto0.ml.html

Source file `g_tuto0.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
let __coq_plugin_name = "tuto0_plugin"
let _ = Mltop.add_known_module __coq_plugin_name

# 3 "doc/plugin_tutorial/tuto0/src/g_tuto0.mlg"
 

open Pp
open Ltac_plugin

let tuto_warn = CWarnings.create ~name:"name" ~category:"category"
                            (fun _ -> strbrk Tuto0_main.message)



let () = Vernacextend.vernac_extend ~command:"HelloWorld" ~classifier:(fun _ -> Vernacextend.classify_as_query) ?entry:None 
         [(Vernacextend.TyML (false, Vernacextend.TyTerminal ("HelloWorld", 
                                     Vernacextend.TyNil), (let coqpp_body () = 
                                                          Vernacextend.vtdefault (fun () -> 
                                                          
# 20 "doc/plugin_tutorial/tuto0/src/g_tuto0.mlg"
                        Feedback.msg_notice (strbrk Tuto0_main.message) 
                                                          ) in fun ?loc ~atts ()
                                                          -> coqpp_body (Attributes.unsupported_attributes atts)), None))]

let () = Tacentries.tactic_extend __coq_plugin_name "hello_world_tactic" ~level:0 
         [(Tacentries.TyML (Tacentries.TyIdent ("hello_world", Tacentries.TyNil), 
           (fun ist -> 
# 28 "doc/plugin_tutorial/tuto0/src/g_tuto0.mlg"
    let _ = Feedback.msg_notice (str Tuto0_main.message) in
    Tacticals.tclIDTAC 
           )))]

let () = Vernacextend.vernac_extend ~command:"HelloWarning" ~classifier:(fun _ -> Vernacextend.classify_as_query) ?entry:None 
         [(Vernacextend.TyML (false, Vernacextend.TyTerminal ("HelloWarning", 
                                     Vernacextend.TyNil), (let coqpp_body () = 
                                                          Vernacextend.vtdefault (fun () -> 
                                                          
# 41 "doc/plugin_tutorial/tuto0/src/g_tuto0.mlg"
    
     tuto_warn ()
   
                                                          ) in fun ?loc ~atts ()
                                                          -> coqpp_body (Attributes.unsupported_attributes atts)), None))]

let () = Tacentries.tactic_extend __coq_plugin_name "hello_warning_tactic" ~level:0 
         [(Tacentries.TyML (Tacentries.TyIdent ("hello_warning", Tacentries.TyNil), 
           (fun ist -> 
# 51 "doc/plugin_tutorial/tuto0/src/g_tuto0.mlg"
    
     let _ = tuto_warn () in
     Tacticals.tclIDTAC
   
           )))]

let () = Vernacextend.vernac_extend ~command:"HelloError" ~classifier:(fun _ -> Vernacextend.classify_as_query) ?entry:None 
         [(Vernacextend.TyML (false, Vernacextend.TyTerminal ("HelloError", 
                                     Vernacextend.TyNil), (let coqpp_body () = 
                                                          Vernacextend.vtdefault (fun () -> 
                                                          
# 64 "doc/plugin_tutorial/tuto0/src/g_tuto0.mlg"
                        CErrors.user_err (str Tuto0_main.message) 
                                                          ) in fun ?loc ~atts ()
                                                          -> coqpp_body (Attributes.unsupported_attributes atts)), None))]

let () = Tacentries.tactic_extend __coq_plugin_name "hello_error_tactic" ~level:0 
         [(Tacentries.TyML (Tacentries.TyIdent ("hello_error", Tacentries.TyNil), 
           (fun ist -> 
# 72 "doc/plugin_tutorial/tuto0/src/g_tuto0.mlg"
    let _ = CErrors.user_err (str Tuto0_main.message) in
    Tacticals.tclIDTAC 
           )))]

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/src/tuto0_plugin/g_tuto0.ml.html

Source file g_tuto0.ml

Source file `g_tuto0.ml`