blob: e6029cdb721765840f534127212fa97049a88eb5 (
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
|
(****************************************************************************)
(* The Calculus of Inductive Constructions *)
(* *)
(* Projet Coq *)
(* *)
(* INRIA LRI-CNRS ENS-CNRS *)
(* Rocquencourt Orsay Lyon *)
(* *)
(* Coq V6.3 *)
(* July 1st 1999 *)
(* *)
(****************************************************************************)
(* astterm.mli *)
(****************************************************************************)
open Names
open Term
open Evd
open Rawterm
(*
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 : context -> 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 -> context -> Coqast.t -> constr
val constr_of_com : 'c evar_map -> context -> Coqast.t -> constr
val constr_of_com_sort : 'c evar_map -> context -> Coqast.t -> constr
val fconstr_of_com1 : bool -> 'c evar_map -> context -> Coqast.t -> constr
val fconstr_of_com : 'c evar_map -> context -> Coqast.t -> constr
val fconstr_of_com_sort : 'c evar_map -> context -> 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 -> judgement
(* $Id$ *)
|
