Source file `g_tuto3.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 "rocq-plugin-tutorial.tuto3"

# 5 "doc/plugin_tutorial/tuto3/src/g_tuto3.mlg"
 

open Ltac_plugin

open Construction_game

(* This one is necessary, to avoid message about missing wit_string *)
open Stdarg


# 15 "doc/plugin_tutorial/tuto3/src/g_tuto3.ml"

let () = Vernacextend.static_vernac_extend ~plugin:(Some "rocq-plugin-tutorial.tuto3") ~command:"ShowTypeConstruction" ~classifier:(fun ~atts:_ _ -> Vernacextend.classify_as_query) ?entry:None 
         [(Vernacextend.TyML
         (false,
          Vernacextend.TyTerminal ("Tuto3_1", Vernacextend.TyNil),
          (let coqpp_body () = Vernactypes.vtdefault (fun () -> 
# 18 "doc/plugin_tutorial/tuto3/src/g_tuto3.mlg"
    let env = Global.env () in
    let sigma = Evd.from_env env in
    let sigma, s = Evd.new_sort_variable Evd.univ_rigid sigma in
    let new_type_2 = EConstr.mkSort s in
    let sigma, _ =
      Typing.type_of env (Evd.from_env env) new_type_2 in
    Feedback.msg_notice
      (Printer.pr_econstr_env env sigma new_type_2) 
# 31 "doc/plugin_tutorial/tuto3/src/g_tuto3.ml"
) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "rocq-plugin-tutorial.tuto3") ~command:"ShowOneConstruction" ~classifier:(fun ~atts:_ _ -> Vernacextend.classify_as_query) ?entry:None 
         [(Vernacextend.TyML
         (false,
          Vernacextend.TyTerminal ("Tuto3_2", Vernacextend.TyNil),
          (let coqpp_body () = Vernactypes.vtdefault (fun () -> 
# 29 "doc/plugin_tutorial/tuto3/src/g_tuto3.mlg"
                     example_sort_app_lambda () 
# 44 "doc/plugin_tutorial/tuto3/src/g_tuto3.ml"
) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]

let () = Tacentries.tactic_extend "rocq-plugin-tutorial.tuto3" "collapse_hyps" ~level:0 
         [(Tacentries.TyML (Tacentries.TyIdent ("pack", Tacentries.TyIdent ("hypothesis", 
                                                        Tacentries.TyArg (
                                                        Extend.TUentry (Genarg.get_arg_tag wit_ident), 
                                                        Tacentries.TyNil))), 
           (fun i ist -> 
# 34 "doc/plugin_tutorial/tuto3/src/g_tuto3.mlg"
    Tuto_tactic.pack_tactic i 
# 58 "doc/plugin_tutorial/tuto3/src/g_tuto3.ml"
)))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "rocq-plugin-tutorial.tuto3") ~command:"TriggerClasses" ~classifier:(fun ~atts:_ _ -> Vernacextend.classify_as_query) ?entry:None 
         [(Vernacextend.TyML
         (false,
          Vernacextend.TyTerminal
          ("Tuto3_3",
           Vernacextend.TyNonTerminal (Extend.TUentry (Genarg.get_arg_tag wit_int),
           Vernacextend.TyNil)),
          (let coqpp_body n () = Vernactypes.vtdefault (fun () -> 
# 41 "doc/plugin_tutorial/tuto3/src/g_tuto3.mlg"
                            example_classes n 
# 71 "doc/plugin_tutorial/tuto3/src/g_tuto3.ml"
) in
            fun n ?loc ~atts () ->
            coqpp_body n (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "rocq-plugin-tutorial.tuto3") ~command:"TriggerCanonical" ~classifier:(fun ~atts:_ _ -> Vernacextend.classify_as_query) ?entry:None 
         [(Vernacextend.TyML
         (false,
          Vernacextend.TyTerminal
          ("Tuto3_4",
           Vernacextend.TyNonTerminal (Extend.TUentry (Genarg.get_arg_tag wit_int),
           Vernacextend.TyNil)),
          (let coqpp_body n () = Vernactypes.vtdefault (fun () -> 
# 46 "doc/plugin_tutorial/tuto3/src/g_tuto3.mlg"
                            example_canonical n 
# 87 "doc/plugin_tutorial/tuto3/src/g_tuto3.ml"
) in
            fun n ?loc ~atts () ->
            coqpp_body n (Attributes.unsupported_attributes atts)),
          None))]