package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/src/ltac2_ltac1_plugin/g_ltac2_ltac1.ml.html
Source file g_ltac2_ltac1.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
let _ = Mltop.add_known_module "rocq-runtime.plugins.ltac2_ltac1" # 13 "plugins/ltac2_ltac1/g_ltac2_ltac1.mlg" open Procq.Prim open Ltac2_plugin open Tac2expr open Ltac_plugin open Ltac2_plugin.G_ltac2 let ltac_expr = Pltac.ltac_expr let inj_wit wit loc x = CAst.make ~loc @@ CTacExt (wit, x) let inj_ltac1 loc e = inj_wit Tac2quote_ltac1.wit_ltac1 loc e let inj_ltac1val loc e = inj_wit Tac2quote_ltac1.wit_ltac1val loc e let _ = let ltac1_expr_in_env = Procq.Entry.make "ltac1_expr_in_env" in let () = Egramml.grammar_extend ~plugin_uid:("rocq-runtime.plugins.ltac2_ltac1", "g_ltac2_ltac1.mlg:0") ltac2_atom (Procq.Reuse (None, [Procq.Production.make (Procq.Rule.next (Procq.Rule.next (Procq.Rule.next (Procq.Rule.next (Procq.Rule.next (Procq.Rule.stop) ((Procq.Symbol.token (Tok.PIDENT (Some ("ltac1val")))))) ((Procq.Symbol.token (Tok.PKEYWORD (":"))))) ((Procq.Symbol.token (Tok.PKEYWORD ("("))))) ((Procq.Symbol.nterm ltac1_expr_in_env))) ((Procq.Symbol.token (Tok.PKEYWORD (")"))))) (fun _ qid _ _ _ loc -> # 34 "plugins/ltac2_ltac1/g_ltac2_ltac1.mlg" inj_ltac1val loc qid ); Procq.Production.make (Procq.Rule.next (Procq.Rule.next (Procq.Rule.next (Procq.Rule.next (Procq.Rule.next (Procq.Rule.stop) ((Procq.Symbol.token (Tok.PIDENT (Some ("ltac1")))))) ((Procq.Symbol.token (Tok.PKEYWORD (":"))))) ((Procq.Symbol.token (Tok.PKEYWORD ("("))))) ((Procq.Symbol.nterm ltac1_expr_in_env))) ((Procq.Symbol.token (Tok.PKEYWORD (")"))))) (fun _ qid _ _ _ loc -> # 33 "plugins/ltac2_ltac1/g_ltac2_ltac1.mlg" inj_ltac1 loc qid )])) in let () = assert (Procq.Entry.is_empty ltac1_expr_in_env) in let () = Egramml.grammar_extend ~plugin_uid:("rocq-runtime.plugins.ltac2_ltac1", "g_ltac2_ltac1.mlg:1") ltac1_expr_in_env (Procq.Fresh (Gramlib.Gramext.First, [(None, None, [Procq.Production.make (Procq.Rule.next (Procq.Rule.stop) ((Procq.Symbol.nterm ltac_expr))) (fun e loc -> # 38 "plugins/ltac2_ltac1/g_ltac2_ltac1.mlg" [], e ); Procq.Production.make (Procq.Rule.next (Procq.Rule.next (Procq.Rule.next (Procq.Rule.next (Procq.Rule.stop) ((Procq.Symbol.nterm test_ltac1_env))) ((Procq.Symbol.list0 (Procq.Symbol.nterm identref)))) ((Procq.Symbol.token (Tok.PKEYWORD ("|-"))))) ((Procq.Symbol.nterm ltac_expr))) (fun e _ ids _ loc -> # 37 "plugins/ltac2_ltac1/g_ltac2_ltac1.mlg" ids, e )])])) in ()
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>