package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c
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