blob: cf2cbfd510f999b2fdaa8d8b0d786e3f4aee978a (
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
|
(*i $Id$ i*)
(*i*)
open Names
open Term
open Sign
open Evd
open Environ
open Rawterm
open Pattern
(*i*)
(* Translation from AST to terms. *)
val interp_rawconstr : 'a evar_map -> env -> Coqast.t -> rawconstr
val interp_constr : 'a evar_map -> env -> Coqast.t -> constr
val interp_casted_constr : 'a evar_map -> env -> Coqast.t -> constr -> constr
val interp_type : 'a evar_map -> env -> Coqast.t -> types
val interp_sort : Coqast.t -> sorts
val interp_openconstr :
'a evar_map -> env -> Coqast.t -> (int * constr) list * constr
val interp_casted_openconstr :
'a evar_map -> env -> Coqast.t -> constr -> (int * constr) list * constr
(* [interp_type_with_implicits] extends [interp_type] by allowing
implicits arguments in the ``rel'' part of [env]; the extra
argument associates a list of implicit positions to identifiers
declared in the rel_context of [env] *)
val interp_type_with_implicits :
'a evar_map -> env ->
(identifier * Impargs.implicits_list) list -> Coqast.t -> types
val judgment_of_rawconstr : 'a evar_map -> env -> Coqast.t -> unsafe_judgment
val type_judgment_of_rawconstr :
'a evar_map -> env -> Coqast.t -> unsafe_type_judgment
(*Interprets a constr according to two lists of instantiations (variables and
metas), possibly casting it*)
val interp_constr_gen :
'a evar_map -> env -> (identifier * constr) list ->
(int * constr) list -> Coqast.t -> constr option -> constr
(*Interprets a constr according to two lists of instantiations (variables and
metas), possibly casting it, and turning unresolved evar into metas*)
val interp_openconstr_gen :
'a evar_map -> env -> (identifier * constr) list ->
(int * constr) list -> Coqast.t -> constr option
-> (int * constr) list * constr
(*Interprets constr patterns according to a list of instantiations
(variables)*)
val interp_constrpattern_gen :
'a evar_map -> env -> (identifier * constr) list -> Coqast.t ->
int list * constr_pattern
val interp_constrpattern :
'a evar_map -> env -> Coqast.t -> int list * constr_pattern
(*s Globalization of AST quotations (mainly used to get statically
bound idents in grammar or pretty-printing rules) *)
val globalize_constr : Coqast.t -> Coqast.t
val globalize_ast : Coqast.t -> Coqast.t
(* This transforms args of a qualid keyword into a qualified ident *)
(* it does no relocation *)
val interp_qualid : Coqast.t list -> Nametab.qualid
(* Translation rules from V6 to V7:
constr_of_com_casted -> interp_casted_constr
constr_of_com_sort -> interp_type
constr_of_com -> interp_constr
rawconstr_of_com -> interp_rawconstr [+ env instead of sign]
type_of_com -> types_of_com Evd.empty
constr_of_com1 true -> interp_type
*)
|
