blob: f6188f536417a3a6d78fc5220f1a0f1fd2c54bd6 (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Names
open Term
open Mod_subst
(** [constr_substituted] are [constr] with possibly pending
substitutions of kernel names. *)
type constr_substituted
val from_val : constr -> constr_substituted
val force : constr_substituted -> constr
val subst_constr_subst :
substitution -> constr_substituted -> constr_substituted
(** Opaque proof terms might be in some external tables. The
[force_opaque] function below allows to access these tables,
this might trigger the read of some extra parts of .vo files *)
type lazy_constr
(** From a [constr] to some (immediate) [lazy_constr]. *)
val opaque_from_val : constr -> lazy_constr
(** Turn an immediate [lazy_constr] into an indirect one, thanks
to the indirect opaque creator configured below. *)
val turn_indirect : lazy_constr -> lazy_constr
(** From a [lazy_constr] back to a [constr]. This might use the
indirect opaque accessor configured below. *)
val force_opaque : lazy_constr -> constr
val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr
val hcons_lazy_constr : lazy_constr -> lazy_constr
(** When stored indirectly, opaque terms are indexed by their library
dirpath and an integer index. The following two functions activate
this indirect storage, by telling how to store and retrieve terms.
Default creator always returns [None], preventing the creation of
any indirect link, and default accessor always raises an error.
*)
val set_indirect_opaque_creator : (constr -> (DirPath.t * int) option) -> unit
val set_indirect_opaque_accessor : (DirPath.t -> int -> constr) -> unit
val reset_indirect_opaque_creator : unit -> unit
|
