blob: a20b1eb3f40a2f58e7325d5d6cbdb9537e4d3f52 (
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
|
(* $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 *)
val ise_resolve : bool -> 'a evar_map -> (int * constr) list ->
env -> 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_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 -> rawconstr -> unsafe_judgment
(*i*)
|
