package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.20.0.tar.gz
md5=66e57ea55275903bef74d5bf36fbe0f1
sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b
doc/src/coq-core.toplevel/g_toplevel.ml.html
Source file g_toplevel.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 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132# 13 "toplevel/g_toplevel.mlg" open Pcoq open Pcoq.Prim open Vernacexpr (* Vernaculars specific to the toplevel *) type vernac_toplevel = | VernacBackTo of int | VernacDrop | VernacQuit | VernacControl of vernac_control | VernacShowGoal of { gid : int; sid: int } | VernacShowProofDiffs of Proof_diffs.diffOpt let vernac_toplevel = Entry.make "toplevel:vernac_toplevel" let err () = raise Gramlib.Stream.Failure let test_show_goal = let open Pcoq.Lookahead in to_entry "test_show_goal" begin lk_kw "Show" >> lk_kw "Goal" >> lk_nat end let _ = let () = Pcoq.grammar_extend vernac_toplevel (Pcoq.Fresh (Gramlib.Gramext.First, [(None, None, [Pcoq.Production.make (Pcoq.Rule.next (Pcoq.Rule.stop) ((Pcoq.Symbol.nterm Pvernac.Vernac_.main_entry))) (fun cmd loc -> # 53 "toplevel/g_toplevel.mlg" match cmd with | None -> None | Some v -> Some (VernacControl v) ); Pcoq.Production.make (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) ((Pcoq.Symbol.token (Tok.PIDENT (Some ("Show")))))) ((Pcoq.Symbol.token (Tok.PIDENT (Some ("Proof")))))) ((Pcoq.Symbol.token (Tok.PIDENT (Some ("Diffs")))))) ((Pcoq.Symbol.opt (Pcoq.Symbol.rules [Pcoq.Rules.make (Pcoq.Rule.next_norec (Pcoq.Rule.stop) ((Pcoq.Symbol.token (Tok.PIDENT (Some ("removed")))))) (fun _ loc -> # 49 "toplevel/g_toplevel.mlg" () )])))) ((Pcoq.Symbol.token (Tok.PKEYWORD ("."))))) (fun _ removed _ _ _ loc -> # 50 "toplevel/g_toplevel.mlg" Some (VernacShowProofDiffs (if removed = None then Proof_diffs.DiffOn else Proof_diffs.DiffRemoved)) ); Pcoq.Production.make (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) ((Pcoq.Symbol.nterm test_show_goal))) ((Pcoq.Symbol.token (Tok.PIDENT (Some ("Show")))))) ((Pcoq.Symbol.token (Tok.PIDENT (Some ("Goal")))))) ((Pcoq.Symbol.nterm natural))) ((Pcoq.Symbol.token (Tok.PIDENT (Some ("at")))))) ((Pcoq.Symbol.nterm natural))) ((Pcoq.Symbol.token (Tok.PKEYWORD ("."))))) (fun _ sid _ gid _ _ _ loc -> # 48 "toplevel/g_toplevel.mlg" Some (VernacShowGoal {gid; sid}) ); Pcoq.Production.make (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) ((Pcoq.Symbol.token (Tok.PIDENT (Some ("BackTo")))))) ((Pcoq.Symbol.nterm natural))) ((Pcoq.Symbol.token (Tok.PKEYWORD ("."))))) (fun _ n _ loc -> # 45 "toplevel/g_toplevel.mlg" Some (VernacBackTo n) ); Pcoq.Production.make (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) ((Pcoq.Symbol.token (Tok.PIDENT (Some ("Quit")))))) ((Pcoq.Symbol.token (Tok.PKEYWORD ("."))))) (fun _ _ loc -> # 43 "toplevel/g_toplevel.mlg" Some VernacQuit ); Pcoq.Production.make (Pcoq.Rule.next (Pcoq.Rule.next (Pcoq.Rule.stop) ((Pcoq.Symbol.token (Tok.PIDENT (Some ("Drop")))))) ((Pcoq.Symbol.token (Tok.PKEYWORD ("."))))) (fun _ _ loc -> # 42 "toplevel/g_toplevel.mlg" Some VernacDrop )])])) in () # 61 "toplevel/g_toplevel.mlg" let vernac_toplevel pm = Pvernac.Unsafe.set_tactic_entry pm; vernac_toplevel