package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.1.tar.gz
md5=13d2793fc6413aac5168822313e4864e
sha512=ec8379df34ba6e72bcf0218c66fef248b0e4c5c436fb3f2d7dd83a2c5f349dd0874a67484fcf9c0df3e5d5937d7ae2b2a79274725595b4b0065a381f70769b42
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