ser_tac2quote.ml
Astdump_plugin
Count_genargs_plugin
Example_plugin
Explain_errors
Goaldumpl_plugin
Metanejo_plugin
Savevo_plugin
Unidiff_plugin
baseline
coq-lsp.coq
coq-lsp.fleche
coq-lsp.lang
coq-lsp.layout-printer
coq-lsp.lsp
coq-lsp.petanque
coq-lsp.plugin
coq-lsp.request
coq-lsp.serlib
fleche_waterproof
petanque_json
petanque_shell
serlib_btauto
serlib_cc
serlib_cc_core
serlib_extraction
serlib_firstorder
serlib_firstorder_core
serlib_funind
serlib_ltac
serlib_ltac2
serlib_ltac2_ltac1
serlib_micromega
serlib_micromega_core
serlib_nsatz_core
serlib_number_string_notation_plugin
serlib_ring
serlib_ssr
serlib_ssrmatching
serlib_tauto
serlib_zify
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 (************************************************************************) (* SerAPI: Coq interaction protocol with bidirectional serialization *) (************************************************************************) (* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *) (* Copyright 2019-2023 Inria -- License LGPL 2.1+ *) (* Written by: Emilio J. Gallego Arias and others *) (************************************************************************) (* open Sexplib.Std *) (* open Ppx_hash_lib.Std.Hash.Builtin *) (* open Ppx_compare_lib.Builtin *) (* let b x = Obj.magic x *) (* These are all special ltac2 extensible objects, brrrr... *) let register () = (* Ser_genarg.register_genser Tac2quote.wit_constr (b()); *) (* Ser_genarg.register_genser Tac2quote.wit_ident (b()); *) (* Ser_genarg.register_genser Tac2quote.wit_ltac1 (b()); *) (* Ser_genarg.register_genser Tac2quote.wit_ltac1val (b()); *) (* Ser_genarg.register_genser Tac2quote.wit_open_constr (b()); *) (* Ser_genarg.register_genser Tac2quote.wit_pattern (b()); *) (* Ser_genarg.register_genser Tac2quote.wit_preterm (b()); *) (* Ser_genarg.register_genser Tac2quote.wit_reference (b()); *) () let () = register ()
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
(************************************************************************) (* SerAPI: Coq interaction protocol with bidirectional serialization *) (************************************************************************) (* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *) (* Copyright 2019-2023 Inria -- License LGPL 2.1+ *) (* Written by: Emilio J. Gallego Arias and others *) (************************************************************************) (* open Sexplib.Std *) (* open Ppx_hash_lib.Std.Hash.Builtin *) (* open Ppx_compare_lib.Builtin *) (* let b x = Obj.magic x *) (* These are all special ltac2 extensible objects, brrrr... *) let register () = (* Ser_genarg.register_genser Tac2quote.wit_constr (b()); *) (* Ser_genarg.register_genser Tac2quote.wit_ident (b()); *) (* Ser_genarg.register_genser Tac2quote.wit_ltac1 (b()); *) (* Ser_genarg.register_genser Tac2quote.wit_ltac1val (b()); *) (* Ser_genarg.register_genser Tac2quote.wit_open_constr (b()); *) (* Ser_genarg.register_genser Tac2quote.wit_pattern (b()); *) (* Ser_genarg.register_genser Tac2quote.wit_preterm (b()); *) (* Ser_genarg.register_genser Tac2quote.wit_reference (b()); *) () let () = register ()