blob: b7a04f644644f7ccdcb3f2f23c4ccf5ff39b6b88 (
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
|
(*i $Id$ i*)
(*i*)
open Names
open Term
open Evd
open Environ
open Inductive
open Rawterm
open Evarutil
(*i*)
(* Used for old cases in pretyping *)
val branch_scheme :
env -> 'a evar_defs -> bool -> inductive_family -> constr array
val pred_case_ml_onebranch : env -> 'c evar_map -> bool ->
inductive_type -> int * constr * constr -> constr
(*i Utilisés dans Program
val pred_case_ml : env -> 'c evar_map -> bool ->
constr * (inductive * constr list * constr list)
-> constr array -> int * constr ->constr
val make_case_ml :
bool -> constr -> constr -> case_info -> constr array -> constr
i*)
(* Compilation of pattern-matching. *)
val compile_cases :
loc -> (type_constraint -> env -> rawconstr -> unsafe_judgment)
* 'a evar_defs -> type_constraint -> env ->
rawconstr option * rawconstr list *
(identifier list * cases_pattern list * rawconstr) list ->
unsafe_judgment
|
