package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.0.tar.gz

sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250

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
let _ = Mltop.add_known_module "coq-plugin-tutorial.tuto0"

# 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 ~plugin:"coq-plugin-tutorial.tuto0" ~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-tutorial.tuto0" "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 ~plugin:"coq-plugin-tutorial.tuto0" ~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-tutorial.tuto0" "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 ~plugin:"coq-plugin-tutorial.tuto0" ~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-tutorial.tuto0" "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-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/src/tuto0_plugin/g_tuto0.ml.html

Source file g_tuto0.ml

Source file `g_tuto0.ml`