package coq-catt-plugin
A Coq plugin for the catt proof-assistant
Install
Dune Dependency
Authors
Maintainers
Sources
catt-1.0.tbz
sha256=20a0b4aae3655274cb7336cb158699ceb1ee29909e50405d0ccb9d54d985baeb
sha512=1919da8eea60817a0907be4aa6f399a9e66fc8746d190ea805de8721a44f5f8a68b9c67626b7767e42a7cd0f061e00c16cd6c63570cbdedf15bc31f8b598f72b
doc/src/coq-catt-plugin.lib/g_catt.ml.html
Source file g_catt.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
let _ = Mltop.add_known_module "coq-catt-plugin.lib" # 3 "coq_plugin/src/g_catt.mlg" open Stdarg let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-catt-plugin.lib") ~command:"Catt" ~classifier:(fun _ -> Vernacextend.classify_as_query) ?entry:None [(Vernacextend.TyML (false, Vernacextend.TyTerminal ("Catt", Vernacextend.TyNonTerminal (Extend.TUlist1 ( Extend.TUentry (Genarg.get_arg_tag wit_string)), Vernacextend.TyTerminal ("From", Vernacextend.TyTerminal ("File", Vernacextend.TyNonTerminal (Extend.TUentry (Genarg.get_arg_tag wit_string), Vernacextend.TyNil))))), (let coqpp_body tms file () = Vernactypes.vtdefault (fun () -> # 8 "coq_plugin/src/g_catt.mlg" Export.catt_tm file tms ) in fun tms file ?loc ~atts () -> coqpp_body tms file (Attributes.unsupported_attributes atts)), None))]
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>