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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
open Tac2expr
(** {5 Hardwired data} *)
module Core :
sig
val t_unit : type_constant
val v_unit : Tac2val.valexpr
val t_list : type_constant
val c_nil : ltac_constructor
val c_cons : ltac_constructor
val t_int : type_constant
val t_option : type_constant
val t_string : type_constant
val t_array : type_constant
val c_true : ltac_constructor
val c_false : ltac_constructor
end
val throw : ?info:Exninfo.info -> exn -> 'a Proofview.tactic
val pf_apply : ?catch_exceptions:bool -> (Environ.env -> Evd.evar_map -> 'a Proofview.tactic) -> 'a Proofview.tactic
module type MapType = sig
(** to have less boilerplate we use S.elt rather than declaring a toplevel type t *)
module S : CSig.USetS
module M : CMap.UExtS with type key = S.elt and module Set := S
type valmap
val valmap_eq : (valmap, Tac2val.valexpr M.t) Util.eq
val repr : S.elt Tac2ffi.repr
end
type ('a,'set,'map) map_tag
type any_map_tag = Any : _ map_tag -> any_map_tag
type tagged_set = TaggedSet : (_,'set,_) map_tag * 'set -> tagged_set
type tagged_map = TaggedMap : (_,_,'map) map_tag * 'map -> tagged_map
val map_tag_repr : any_map_tag Tac2ffi.repr
val set_repr : tagged_set Tac2ffi.repr
val map_repr : tagged_map Tac2ffi.repr
val register_map : ?plugin:string -> tag_name:string
-> (module MapType with type S.elt = 'a and type S.t = 'set and type valmap = 'map)
-> ('a,'set,'map) map_tag
(** Register a type on which we can use finite sets and maps.
[tag_name] is the name used for the external to make the
[Ltac2.FSet.Tags.tag] available. *)
(** Default registered maps *)
val ident_map_tag : (Id.t, Id.Set.t, Tac2val.valexpr Id.Map.t) map_tag
val int_map_tag : (int, Int.Set.t, Tac2val.valexpr Int.Map.t) map_tag
val string_map_tag : (string, CString.Set.t, Tac2val.valexpr CString.Map.t) map_tag
val inductive_map_tag : (inductive, Indset_env.t, Tac2val.valexpr Indmap_env.t) map_tag
val constructor_map_tag : (constructor, Constrset_env.t, Tac2val.valexpr Constrmap_env.t) map_tag
val constant_map_tag : (Constant.t, Cset_env.t, Tac2val.valexpr Cmap_env.t) map_tag
|
