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

(limited to 'kernel/inferCumulativity.ml')

diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index d02f92ef26..50c3ba1cc6 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -198,7 +198,9 @@ let rec infer_fterm cv_pb infos variances hd stk =
     let variances = infer_vect infos variances elems in
     infer_stack infos variances stk
 
-  | FCaseInvert (_,p,_,_,br,e) ->
+  | FCaseInvert (ci, u, pms, p, _, _, br, e) ->
+    let mib = Environ.lookup_mind (fst ci.ci_ind) (info_env (fst infos)) in
+    let (_, p, _, _, br) = Inductive.expand_case_specif mib (ci, u, pms, p, NoInvert, mkProp, br) in
     let infer c variances = infer_fterm CONV infos variances (mk_clos e c) [] in
     let variances = infer p variances in
     Array.fold_right infer br variances
@@ -217,7 +219,10 @@ and infer_stack infos variances (stk:CClosure.stack) =
       | Zfix (fx,a) ->
         let variances = infer_fterm CONV infos variances fx [] in
         infer_stack infos variances a
-      | ZcaseT (_, p, br, e) ->
+      | ZcaseT (ci,u,pms,p,br,e) ->
+        let dummy = mkProp in
+        let case = (ci, u, pms, p, NoInvert, dummy, br) in
+        let (_, p, _, _, br) = Inductive.expand_case (info_env (fst infos)) case in
         let variances = infer_fterm CONV infos variances (mk_clos e p) [] in
         infer_vect infos variances (Array.map (mk_clos e) br)
       | Zshift _ -> variances
-- 
cgit v1.2.3