From b053d98fb17d2f46878f49d7adf4839ae632c10b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 15 May 2018 21:51:21 +0200
Subject: Remove vm_conv hook and reorganize kernel files

---
 kernel/reduction.mli | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'kernel/reduction.mli')

diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 14e4270b7c..2e10f98c57 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -87,10 +87,6 @@ val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) ->
 val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) ->
   Names.transparent_state -> (constr,'a) generic_conversion_function
 
-(** option for conversion *)
-val set_vm_conv : (conv_pb -> types kernel_conversion_function) -> unit
-val vm_conv : conv_pb -> types kernel_conversion_function
-
 val default_conv     : conv_pb -> ?l2r:bool -> types kernel_conversion_function
 val default_conv_leq : ?l2r:bool -> types kernel_conversion_function
 
@@ -128,5 +124,3 @@ exception NotArity
 
 val dest_arity : env -> types -> Term.arity (* raises NotArity if not an arity *)
 val is_arity   : env -> types -> bool
-
-val warn_bytecode_compiler_failed : ?loc:Loc.t -> unit -> unit
-- 
cgit v1.2.3


From 442bd1fe4007d2f3b46cb565abbcd64011db1af4 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 16 May 2018 00:36:08 +0200
Subject: Fix #7333: vm_compute segfaults / Anomaly with cofix

We eta-expand cofixpoints when needed, so that their call-by-need
evaluation is correctly implemented by VM and native_compute.
---
 kernel/reduction.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/reduction.mli')

diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 2e10f98c57..e53ab6aefb 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -118,9 +118,12 @@ val betazeta_appvect : int -> constr -> constr array -> constr
 
 val dest_prod       : env -> types -> Context.Rel.t * types
 val dest_prod_assum : env -> types -> Context.Rel.t * types
+val dest_lam        : env -> types -> Context.Rel.t * constr
 val dest_lam_assum  : env -> types -> Context.Rel.t * types
 
 exception NotArity
 
 val dest_arity : env -> types -> Term.arity (* raises NotArity if not an arity *)
 val is_arity   : env -> types -> bool
+
+val eta_expand : env -> constr -> types -> constr
-- 
cgit v1.2.3