aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/vconv.mli
blob: 21fd4601b17fad43b2b95b821412d27c30ff4e4c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
(*i*)
open Names
open Term
open Environ
open Reduction
(*i*)

(***********************************************************************)
(*s conversion functions *)
val vconv : conv_pb -> types conversion_function

(***********************************************************************)
(*s Reduction functions *)
val cbv_vm : env -> constr -> types -> constr