blob: f46f9ddb3d264d60c5a4700b5d0a1d33415d3d7c (
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
|
(* $Id$ *)
(*i*)
open Names
open Sign
open Term
open Environ
open Evd
open Rawterm
open Evarutil
(*i*)
(* Raw calls to the inference machine of Trad: boolean says if we must fail
on unresolved evars, or replace them by Metas ; the [unsafe_judgment] list
allows us to extend env with some bindings *)
val ise_resolve : bool -> 'a evar_map -> (int * constr) list ->
env -> (identifier * unsafe_judgment) list ->
(int * unsafe_judgment) list -> rawconstr -> unsafe_judgment
val ise_resolve_type : bool -> 'a evar_map -> (int * constr) list ->
env -> rawconstr -> typed_type
(* Call [ise_resolve] with empty metamap and [fail_evar=true]. The boolean says
* if we must coerce to a type *)
val ise_resolve1 : bool -> 'a evar_map -> env -> rawconstr -> constr
val ise_resolve2 : 'a evar_map -> env -> (identifier * unsafe_judgment) list ->
(int * unsafe_judgment) list -> rawconstr -> constr
val ise_resolve_casted_gen :
'a evar_map -> env -> (identifier * unsafe_judgment) list ->
(int * unsafe_judgment) list -> constr -> rawconstr -> constr
val ise_resolve_casted : 'a evar_map -> env -> constr -> rawconstr -> constr
(* progmach.ml tries to type ill-typed terms: does not perform the conversion
* test in application.
*)
val ise_resolve_nocheck : 'a evar_map -> (int * constr) list ->
env -> rawconstr -> unsafe_judgment
(* Typing with Trad, and re-checking with Mach *)
(*i
val infconstruct_type :
'c evar_map -> (env * env) ->
Coqast.t -> typed_type * information
val infconstruct :
'c evar_map -> (env * env) ->
Coqast.t -> unsafe_judgment * information
(* Typing, re-checking with universes constraints *)
val fconstruct_with_univ :
'c evar_map -> env -> Coqast.t -> unsafe_judgment
val fconstruct_with_univ_sp : 'c evar_map -> env
-> section_path -> constr -> Impuniv.universes * unsafe_judgment
val fconstruct_type_with_univ_sp : 'c evar_map -> env
-> section_path -> constr -> Impuniv.universes * typed_type
val infconstruct_with_univ_sp :
'c evar_map -> (env * env)
-> section_path -> constr -> Impuniv.universes * (unsafe_judgment * information)
val infconstruct_type_with_univ_sp :
'c evar_map -> (env * env)
-> section_path -> constr
-> Impuniv.universes * (typed_type * information)
i*)
(*i*)
(* Internal of Trad...
* Unused outside Trad, but useful for debugging
*)
val pretype :
trad_constraint -> env -> 'a evar_defs ->
(identifier * unsafe_judgment) list -> (int * unsafe_judgment) list ->
rawconstr -> unsafe_judgment
(*i*)
|
