blob: a07eed5659847b911be5bf4a6e106e8b0a995623 (
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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* Certification of Imperative Programs / Jean-Christophe Filliâtre *)
(* $Id$ *)
open Names
open Term
open Ptype
open Topconstr
(* Some misc. functions *)
val reraise_with_loc : Util.loc -> ('a -> 'b) -> 'a -> 'b
val list_of_some : 'a option -> 'a list
val difference : 'a list -> 'a list -> 'a list
val at_id : identifier -> string -> identifier
val un_at : identifier -> identifier * string
val is_at : identifier -> bool
val result_id : identifier
val adr_id : identifier -> identifier
val renaming_of_ids : identifier list -> identifier list
-> (identifier * identifier) list * identifier list
val reset_names : unit -> unit
val pre_name : name -> identifier
val post_name : name -> identifier
val inv_name : name -> identifier
val test_name : name -> identifier
val bool_name : unit -> identifier
val var_name : name -> identifier
val phi_name : unit -> identifier
val for_name : unit -> identifier
val label_name : unit -> string
val id_of_name : name -> identifier
(* CIC terms *)
val isevar : constr
val subst_in_constr : (identifier * identifier) list -> constr -> constr
val subst_in_ast : (identifier * identifier) list -> constr_expr -> constr_expr
val subst_ast_in_ast :
(identifier * constr_expr) list -> constr_expr -> constr_expr
val real_subst_in_constr : (identifier * constr) list -> constr -> constr
val constant : string -> constr
val coq_constant : string list -> string -> kernel_name
val conj : constr -> constr -> constr
val coq_true : constr
val coq_false : constr
val connective_and : identifier
val connective_or : identifier
val connective_not : identifier
val is_connective : identifier -> bool
val n_mkNamedProd : constr -> (identifier * constr) list -> constr
val n_lambda : constr -> (identifier * constr) list -> constr
val abstract : (identifier * constr) list -> constr -> constr
val type_v_knsubst : substitution -> type_v -> type_v
val type_c_knsubst : substitution -> type_c -> type_c
(* for debugging purposes *)
val deb_mess : Pp.std_ppcmds -> unit
val deb_print : ('a -> Pp.std_ppcmds) -> 'a -> unit
|
