blob: 98716046f2eca6e0b98a67099d0aa23ab5715341 (
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
|
(* $Id$ *)
(*i*)
open Pp
open Names
open Term
open Evd
open Environ
open Libobject
open Declare
(*i*)
type cl_typ =
| CL_SORT
| CL_FUN
| CL_Var of identifier
| CL_SP of section_path
| CL_IND of section_path * int
type cl_info_typ = {
cL_STR : string;
cL_STRE : strength;
cL_PARAM : int }
type cte_typ =
| NAM_Var of identifier
| NAM_SP of section_path
| NAM_Construct of section_path * int * int
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 cte_of_constr : constr -> cte_typ
val class_info : cl_typ -> (int * cl_info_typ)
val coercion_info : coe_typ -> (int * coe_info_typ)
val constructor_at_head : constr -> cl_typ * int
val class_of : '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 print_graph : unit -> (int * string) Pp.ppcmd_token Stream.t
val print_classes : unit -> (int * string) Pp.ppcmd_token Stream.t
val print_coercions : unit -> (int * string) Pp.ppcmd_token Stream.t
val print_path_between : identifier -> identifier -> (int * string) ppcmd_token Stream.t
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
|
