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
73
74
75
76
77
78
79
80
81
82
83
84
85
let _ = Mltop.add_known_module "rocq-plugin-tutorial.plugin"

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

open Pp
open Ltac_plugin

let cat = CWarnings.create_category ~name:"plugin-tuto-cat" ()

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


# 16 "doc/plugin_tutorial/tuto0/src/g_tuto0.ml"

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

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

let () = Vernacextend.static_vernac_extend ~plugin:(Some "rocq-plugin-tutorial.plugin") ~command:"HelloWarning" ~classifier:(fun ~atts:_ _ -> Vernacextend.classify_as_query) ?entry:None 
         [(Vernacextend.TyML
         (false,
          Vernacextend.TyTerminal ("HelloWarning", Vernacextend.TyNil),
          (let coqpp_body () = Vernactypes.vtdefault (fun () -> 
# 45 "doc/plugin_tutorial/tuto0/src/g_tuto0.mlg"
    
     tuto_warn ()
   
# 49 "doc/plugin_tutorial/tuto0/src/g_tuto0.ml"
) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]

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

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

let () = Tacentries.tactic_extend "rocq-plugin-tutorial.plugin" "hello_error_tactic" ~level:0 
         [(Tacentries.TyML (Tacentries.TyIdent ("hello_error", Tacentries.TyNil), 
           (fun ist -> 
# 76 "doc/plugin_tutorial/tuto0/src/g_tuto0.mlg"
    CErrors.user_err (str Tuto0_main.message) 
# 84 "doc/plugin_tutorial/tuto0/src/g_tuto0.ml"
)))]