blob: 6c50a5ebd5535fc13799b2388c79398773736e48 (
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
|
(* $Id$ *)
(*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 -> constr
val typed_type_of_com : 'a evar_map -> env -> Coqast.t -> typed_type
val judgment_of_com : 'a evar_map -> env -> Coqast.t -> unsafe_judgment
val interp_sort : Coqast.t -> sorts
(*Interprets a constr according to two lists of instantiations (variables and
metas)*)
val interp_constr1 :
'a evar_map -> env -> (identifier * constr) list ->
(int * constr) list -> Coqast.t -> constr
(*Interprets a casted constr according to two lists of instantiations
(variables and metas)*)
val interp_casted_constr1 :
'a evar_map -> env -> (identifier * constr) list ->
(int * constr) list -> Coqast.t -> constr -> constr
val interp_constrpattern :
'a evar_map -> env -> Coqast.t -> int list * constr_pattern
(* 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 -> typed_type_of_com Evd.empty
constr_of_com1 true -> interp_type
*)
(*i For debug (or obsolete)
val dbize_op : CoqAst.loc -> string -> CoqAst.t list -> constr list -> constr
val dbize : unit assumptions -> CoqAst.t -> constr
val dbize_cci : 'c evar_map -> unit assumptions -> Coqast.t -> rawconstr
val absolutize_cci : 'c evar_map -> unit assumptions -> constr -> constr
val dbize_fw : 'c evar_map -> unit assumptions -> Coqast.t -> rawconstr
val absolutize_fw : 'c evar_map -> unit assumptions -> constr -> constr
val raw_fconstr_of_com :
'c evar_map -> 'a assumptions -> Coqast.t -> rawconstr
val fconstr_of_com : 'a evar_map -> env -> Coqast.t -> constr
val fconstr_of_com_sort : 'a evar_map -> env -> Coqast.t -> constr
val raw_constr_of_compattern :
'c evar_map -> 'a assumptions -> Coqast.t -> rawconstr
*)
val globalize_command : Coqast.t -> Coqast.t
(*
val globalize_ast : Coqast.t -> Coqast.t
(* Typing with Trad, and re-checking with Mach *)
val fconstruct :'c evar_map -> context -> Coqast.t -> unsafe_judgment
val fconstruct_type : 'c evar_map -> context -> Coqast.t -> typed_type
(* Typing, re-checking with universes constraints *)
val fconstruct_with_univ :
'a evar_map -> context -> Coqast.t -> unsafe_judgment
i*)
|
