blob: 7c48d28189aba56817eb7f0ddb24e443aa6577e9 (
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
|
(* $Id$ *)
(*i*)
open Names
open Term
open Sign
open Evd
open Environ
open Rawterm
(*i*)
(* Translation from AST to terms. *)
(*
val dbize_op : CoqAst.loc -> string -> CoqAst.t list -> constr list -> constr
val dbize : unit assumptions -> CoqAst.t -> constr
val absolutize_cci : 'c evar_map -> unit assumptions -> constr -> constr
*)
val dbize_cci : 'c evar_map -> unit assumptions -> Coqast.t -> rawconstr
(*
val absolutize_fw : 'c evar_map -> unit assumptions -> constr -> constr
*)
val dbize_fw : 'c evar_map -> unit assumptions -> Coqast.t -> rawconstr
val raw_constr_of_com :
'c evar_map -> 'a assumptions -> Coqast.t -> rawconstr
val raw_fconstr_of_com :
'c evar_map -> 'a assumptions -> Coqast.t -> rawconstr
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
(*i Ceci était avant dans Trad
Maintenant elles sont là car relève des ast i*)
val type_of_com : unsafe_env -> Coqast.t -> typed_type
val constr_of_com_casted : 'c evar_map -> context -> Coqast.t -> constr ->
constr
val constr_of_com1 : bool -> 'c evar_map -> unsafe_env -> Coqast.t -> constr
val constr_of_com : 'c evar_map -> unsafe_env -> Coqast.t -> constr
val constr_of_com_sort : 'c evar_map -> unsafe_env -> Coqast.t -> constr
val fconstr_of_com1 : bool -> 'c evar_map -> unsafe_env -> Coqast.t -> constr
val fconstr_of_com : 'c evar_map -> unsafe_env -> Coqast.t -> constr
val fconstr_of_com_sort : 'c evar_map -> unsafe_env -> Coqast.t -> constr
(* 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 :
'c evar_map -> context -> Coqast.t -> unsafe_judgment
|
