blob: 456df8369955b2b5f498a890eee792e1ab5cb43c (
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
|
open Names
open Cic
val force_constr : constr_substituted -> constr
val force_lazy_constr_univs : Cic.constant_def -> Univ.ContextSet.t
val from_val : constr -> constr_substituted
val indirect_opaque_access : (DirPath.t -> int -> constr) ref
val indirect_opaque_univ_access : (DirPath.t -> int -> Univ.ContextSet.t) ref
(** Constant_body *)
val body_of_constant : constant_body -> constr option
val constant_has_body : constant_body -> bool
val is_opaque : constant_body -> bool
val opaque_univ_context : constant_body -> Univ.ContextSet.t
(* Mutual inductives *)
val mk_norec : wf_paths
val mk_paths : recarg -> wf_paths list array -> wf_paths
val dest_recarg : wf_paths -> recarg
val dest_subterms : wf_paths -> wf_paths list array
val eq_recarg : recarg -> recarg -> bool
val eq_wf_paths : wf_paths -> wf_paths -> bool
(* Modules *)
val empty_delta_resolver : delta_resolver
(* Substitutions *)
type 'a subst_fun = substitution -> 'a -> 'a
val empty_subst : substitution
val add_mbid : MBId.t -> module_path -> substitution -> substitution
val add_mp : module_path -> module_path -> substitution -> substitution
val map_mbid : MBId.t -> module_path -> substitution
val map_mp : module_path -> module_path -> substitution
val mp_in_delta : module_path -> delta_resolver -> bool
val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive
val subst_const_body : constant_body subst_fun
val subst_mind : mutual_inductive_body subst_fun
val subst_signature : substitution -> module_signature -> module_signature
val subst_module : substitution -> module_body -> module_body
val join : substitution -> substitution -> substitution
|
