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
82
83
84
85
86
87
88
89
90
91
92
93
94
|
(************************************************************************)
(* * 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 Environ
open Evd
open EConstr
open Ltac_pretype
open Evarutil
(** Type of environment extended with naming and ltac interpretation data *)
type t
(** To embed constr in glob_constr *)
type 'a obj_interp_fun =
?loc:Loc.t -> poly:bool -> t -> Evd.evar_map -> Evardefine.type_constraint ->
'a -> unsafe_judgment * Evd.evar_map
val register_constr_interp0 :
('r, 'g, 't) Genarg.genarg_type -> 'g obj_interp_fun -> unit
(** {6 Pretyping name management} *)
(** The following provides a level of abstraction for the kind of
environment used for type inference (so-called pretyping); in
particular:
- it supports that term variables can be interpreted as Ltac
variables pointing to the effective expected name
- it incrementally and lazily computes the renaming of rel
variables used to build purely-named evar contexts
*)
(** Build a pretyping environment from an ltac environment *)
val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t
(** Export the underlying environment *)
val env : t -> env
val renamed_env : t -> env
val lfun : t -> unbound_ltac_var_map
val vars_of_env : t -> Id.Set.t
(** Push to the environment, returning the declaration(s) with interpreted names *)
val push_rel : hypnaming:naming_mode -> evar_map -> rel_declaration -> t -> rel_declaration * t
val push_rel_context : hypnaming:naming_mode -> ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t
val push_rec_types : hypnaming:naming_mode -> evar_map -> Name.t Context.binder_annot array * constr array -> t -> Name.t Context.binder_annot array * t
(** Declare an evar using renaming information *)
val new_evar : t -> evar_map -> ?src:Evar_kinds.t Loc.located ->
?naming:Namegen.intro_pattern_naming_expr -> constr -> evar_map * constr
val new_type_evar : t -> evar_map -> src:Evar_kinds.t Loc.located -> evar_map * constr
(** [hide_variable env na id] tells to hide the binding of [id] in
the ltac environment part of [env] and to additionally rebind
it to [id'] in case [na] is some [Name id']. It is useful e.g.
for the dual status of [y] as term and binder. This is the case
of [match y return p with ... end] which implicitly denotes
[match z as z return p with ... end] when [y] is bound to a
variable [z] and [match t as y return p with ... end] when [y]
is bound to a non-variable term [t]. In the latter case, the
binding of [y] to [t] should be hidden in [p]. *)
val hide_variable : t -> Name.t -> Id.t -> t
(** In case a variable is not bound by a term binder, look if it has
an interpretation as a term in the ltac_var_map *)
val interp_ltac_variable : ?loc:Loc.t -> (t -> Glob_term.glob_constr -> evar_map * unsafe_judgment) ->
t -> evar_map -> Id.t -> evar_map * unsafe_judgment
(** Interp an identifier as an ltac variable bound to an identifier,
or as the identifier itself if not bound to an ltac variable *)
val interp_ltac_id : t -> Id.t -> Id.t
(** Interpreting a generic argument, typically a "ltac:(...)", taking
into account the possible renaming *)
val interp_glob_genarg : ?loc:Loc.t -> poly:bool -> t -> evar_map -> Evardefine.type_constraint ->
Genarg.glob_generic_argument -> unsafe_judgment * evar_map
|
