From d72e5c154faeea1d55387bc8c039d97f63ebd1c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 3 Mar 2019 21:03:37 +0100
Subject: Change the representation of kernel case.

We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
---
 kernel/nativelambda.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/nativelambda.ml')

diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index b27c53ef0f..f3b483467d 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -535,7 +535,8 @@ let rec lambda_of_constr cache env sigma c =
     let prefix = get_mind_prefix env (fst ind) in
     mkLapp (Lproj (prefix, ind, Projection.arg p)) [|lambda_of_constr cache env sigma c|]
 
-  | Case(ci,t,_iv,a,branches) -> (* XXX handle iv *)
+  | Case (ci, u, pms, t, iv, a, br) -> (* XXX handle iv *)
+    let (ci, t, _iv, a, branches) = Inductive.expand_case env (ci, u, pms, t, iv, a, br) in
     let (mind,i as ind) = ci.ci_ind in
     let mib = lookup_mind mind env in
     let oib = mib.mind_packets.(i) in
-- 
cgit v1.2.3