blob: 2fc37b2c9f6cef193d9b06aa6d6592c766c49565 (
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
|
(* tacinvutils.ml *)
(*s utilities *)
(*i*)
open Termops
open Equality
open Names
open Pp
open Tacmach
open Proof_type
open Tacinterp
open Tactics
open Tacticals
open Term
open Util
open Printer
open Reductionops
open Inductiveops
open Coqlib
open Refine
open Evd
(*i*)
(* printing debugging *)
val prconstr: constr -> unit
val prlistconstr: constr list -> unit
val prNamedConstr:string -> constr -> unit
val prNamedLConstr:string -> constr list -> unit
val prstr: string -> unit
val mknewmeta: unit -> constr
val mknewexist: unit -> existential
val resetmeta: unit -> unit (* safe *)
val resetexist: unit -> unit (* be careful with this one *)
val mkevarmap_from_listex: (Term.existential * Term.types) list -> evar_map
val mkEq: types -> constr -> constr -> constr
(* let mkEq typ c1 c2 = mkApp (build_coq_eq_data.eq(),[| typ; c1; c2|]) *)
val mkRefl: types -> constr -> constr
val buildrefl_from_eqs: constr list -> constr list
(* typ c1 = mkApp ((constant ["Coq"; "Init"; "Logic"] "refl_equal"), [| typ; c1|]) *)
val nth_dep_constructor: constr -> int -> (constr*int)
val prod_it_lift: (name*constr) list -> constr -> constr
val prod_it_anonym_lift: constr -> constr list -> constr
val lam_it_anonymous: constr -> constr list -> constr
val lift1L: (constr list) -> constr list
val popn: int -> constr -> constr
val lambda_id: constr -> constr -> constr -> constr
val prod_id: constr -> constr -> constr -> constr
val name_of_string : string -> name
val newname_append: name -> string -> name
val apply_eqtrpl: constr*(constr*constr*constr) -> constr -> constr
val substitterm: int -> constr -> constr -> constr -> constr
val apply_leqtrpl_t:
constr -> (constr*(constr*constr*constr)) list -> constr
val apply_eq_leqtrpl:
(constr*(constr*constr*constr)) list -> constr -> (constr*(constr*constr*constr)) list
(* val apply_leq_lt: constr list -> constr list -> constr list *)
val hdMatchSub: constr -> constr -> constr list
val hdMatchSub_cpl: constr -> int*int -> constr list
val exchange_hd_prod: constr -> constr -> constr
val exchange_reli_arrayi_L: constr array -> int*int -> constr list -> constr list
val substit_red: int -> constr -> constr -> constr -> constr
val expand_letins: constr -> constr
val def_of_const: constr -> constr
val name_of_const: constr -> string
(*i
Local Variables:
compile-command: "make -k tacinvutils.cmi"
End:
i*)
|
