blob: 342161cb440877de9e78b1349b966fcd96631e0e (
plain)
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
|
(* $Id$ *)
(*i*)
open Pp
open Names
open Term
open Evd
open Environ
open Libobject
open Declare
open Rawterm
(*i*)
type cl_typ =
| CL_SORT
| CL_FUN
| CL_Var of identifier
| CL_SP of section_path
| CL_IND of inductive_path
type cl_info_typ = {
cL_STR : string;
cL_STRE : strength;
cL_PARAM : int }
type cte_typ =
| NAM_Var of identifier
| NAM_Constant of section_path
| NAM_Inductive of inductive_path
| NAM_Constructor of constructor_path
type coe_typ = cte_typ
type coe_info_typ = {
cOE_VALUE : unsafe_judgment;
cOE_STRE : strength;
cOE_ISID : bool;
cOE_PARAM : int }
type inheritance_path = int list
val inheritance_graph : unit -> ((int * int) * inheritance_path) list
val classes : unit -> (int * (cl_typ * cl_info_typ)) list
val coercions : unit -> (int * (coe_typ * coe_info_typ)) list
val cte_of_constr : constr -> cte_typ
val class_info : cl_typ -> (int * cl_info_typ)
val class_exists : cl_typ -> bool
val class_info_from_index : int -> cl_typ * cl_info_typ
val coercion_exists : coe_typ -> bool
val coercion_info : coe_typ -> (int * coe_info_typ)
val coercion_info_from_index : int -> coe_typ * coe_info_typ
(* [coercion_params] raises [Not_found] if not a coercion *)
val coercion_params : global_reference -> int
val constructor_at_head : constr -> cl_typ * int
(* raises [Not_found] if not convertible to a class *)
val class_of : env -> 'c evar_map -> constr -> constr * int
val class_args_of : constr -> constr list
val inClass : (cl_typ * cl_info_typ) -> obj
val outClass : obj -> (cl_typ * cl_info_typ)
val inCoercion : (coe_typ * coe_info_typ) * cl_typ * cl_typ -> obj
val outCoercion : obj -> (coe_typ * coe_info_typ) * cl_typ * cl_typ
val lookup_path_between : (int * int) -> inheritance_path
val lookup_path_to_fun_from : int -> inheritance_path
val lookup_path_to_sort_from : int -> inheritance_path
val coe_value : int -> (unsafe_judgment * bool)
val arity_sort : constr -> int
val fully_applied : identifier -> int -> int -> unit
val stre_of_cl : cl_typ -> strength
val add_new_class : (cl_typ * string * strength * int) -> unit
val add_new_coercion_in_graph :
(coe_typ * coe_info_typ) * cl_typ * cl_typ -> unit
val add_coercion_in_graph : int * int * int -> unit
val install_path_printer :
((int * int) * inheritance_path -> std_ppcmds) -> unit
|
