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/relevanceops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/relevanceops.ml')

diff --git a/kernel/relevanceops.ml b/kernel/relevanceops.ml
index f12b8cba37..986fc685d1 100644
--- a/kernel/relevanceops.ml
+++ b/kernel/relevanceops.ml
@@ -61,7 +61,7 @@ let rec relevance_of_fterm env extra lft f =
       | FProj (p, _) -> relevance_of_projection env p
       | FFix (((_,i),(lna,_,_)), _) -> (lna.(i)).binder_relevance
       | FCoFix ((i,(lna,_,_)), _) -> (lna.(i)).binder_relevance
-      | FCaseT (ci, _, _, _, _) | FCaseInvert (ci, _, _, _, _, _) -> ci.ci_relevance
+      | FCaseT (ci, _, _, _, _, _, _) | FCaseInvert (ci, _, _, _, _, _, _, _) -> ci.ci_relevance
       | FLambda (len, tys, bdy, e) ->
         let extra = List.fold_left (fun accu (x, _) -> Range.cons (binder_relevance x) accu) extra tys in
         let lft = Esubst.el_liftn len lft in
@@ -97,7 +97,7 @@ and relevance_of_term_extra env extra lft subs c =
   | App (c, _) -> relevance_of_term_extra env extra lft subs c
   | Const (c,_) -> relevance_of_constant env c
   | Construct (c,_) -> relevance_of_constructor env c
-  | Case (ci, _, _, _, _) -> ci.ci_relevance
+  | Case (ci, _, _, _, _, _, _) -> ci.ci_relevance
   | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance
   | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance
   | Proj (p, _) -> relevance_of_projection env p
-- 
cgit v1.2.3