forked from rocq-archive/coq-serapi
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathser_impargs.mli
58 lines (40 loc) · 2.45 KB
/
ser_impargs.mli
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
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(************************************************************************)
(* Coq serialization API/Plugin *)
(* Copyright 2016 MINES ParisTech *)
(************************************************************************)
(* Status: Very Experimental *)
(************************************************************************)
open Sexplib
type argument_position = Impargs.argument_position
val argument_position_of_sexp : Sexp.t -> argument_position
val sexp_of_argument_position : argument_position -> Sexp.t
type implicit_kind = Impargs.implicit_kind
val implicit_kind_of_sexp : Sexp.t -> implicit_kind
val sexp_of_implicit_kind : implicit_kind -> Sexp.t
val implicit_kind_of_yojson : Yojson.Safe.t -> (implicit_kind, string) Result.result
val implicit_kind_to_yojson : implicit_kind -> Yojson.Safe.t
type implicit_explanation = Impargs.implicit_explanation
val implicit_explanation_of_sexp : Sexp.t -> implicit_explanation
val sexp_of_implicit_explanation : implicit_explanation -> Sexp.t
type maximal_insertion = Impargs.maximal_insertion
val maximal_insertion_of_sexp : Sexp.t -> maximal_insertion
val sexp_of_maximal_insertion : maximal_insertion -> Sexp.t
type force_inference = Impargs.force_inference
val force_inference_of_sexp : Sexp.t -> force_inference
val sexp_of_force_inference : force_inference -> Sexp.t
type implicit_side_condition = Impargs.implicit_side_condition
val implicit_side_condition_of_sexp : Sexp.t -> implicit_side_condition
val sexp_of_implicit_side_condition : implicit_side_condition -> Sexp.t
type implicit_status = Impargs.implicit_status
val implicit_status_of_sexp : Sexp.t -> implicit_status
val sexp_of_implicit_status : implicit_status -> Sexp.t
type implicits_list = Impargs.implicits_list
val implicits_list_of_sexp : Sexp.t -> implicits_list
val sexp_of_implicits_list : implicits_list -> Sexp.t