package coq-serapi

  1. Overview
  2. Docs
Serialization library and protocol for machine interaction with the Coq proof assistant

Install

Dune Dependency

Authors

Maintainers

Sources

coq-serapi-8.15.0.0.15.4.tbz
sha256=cffb0eacd9d155434f7cf384418c78a9d1cf189b65b080a456f50d9d3c3dcf5c
sha512=77eada7c9f2979ee8b00704ed49e65f6e0aadb1a24b73bb89581bf624f330d141340e0dfecd8b1517a11b2a9d823d8f84fcbdea419cc99536557019c5951b80e

doc/src/serlib_ltac2/ser_tac2quote.ml.html

Source file ser_tac2quote.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
(* open Serlib *)
(* open Ltac2_plugin *)

(* 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 ()
OCaml

Innovation. Community. Security.