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.
---
 pretyping/typing.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index e3e5244a8c..b0ce4fd63a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -178,7 +178,7 @@ let type_case_branches env sigma (ind,largs) pj c =
   let ty = whd_betaiota env sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in
   sigma, (lc, ty, Sorts.relevance_of_sort ps)
 
-let judge_of_case env sigma ci pj iv cj lfj =
+let judge_of_case env sigma case ci pj iv cj lfj =
   let ((ind, u), spec) =
     try find_mrectype env sigma cj.uj_type
     with Not_found -> error_case_not_inductive env sigma cj in
@@ -189,7 +189,7 @@ let judge_of_case env sigma ci pj iv cj lfj =
   let () = if (match iv with | NoInvert -> false | CaseInvert _ -> true) != should_invert_case env ci
     then Type_errors.error_bad_invert env
   in
-  sigma, { uj_val  = mkCase (ci, pj.uj_val, iv, cj.uj_val, Array.map j_val lfj);
+  sigma, { uj_val  = mkCase case;
            uj_type = rslty }
 
 let check_type_fixpoint ?loc env sigma lna lar vdefj =
@@ -383,7 +383,9 @@ let rec execute env sigma cstr =
         let sigma, ty = type_of_constructor env sigma ctor in
         sigma, make_judge cstr ty
 
-    | Case (ci,p,iv,c,lf) ->
+    | Case (ci, u, pms, p, iv, c, lf) ->
+        let case = (ci, u, pms, p, iv, c, lf) in
+        let (ci, p, iv, c, lf) = EConstr.expand_case env sigma case in
         let sigma, cj = execute env sigma c in
         let sigma, pj = execute env sigma p in
         let sigma, lfj = execute_array env sigma lf in
@@ -396,7 +398,7 @@ let rec execute env sigma cstr =
             let sigma = check_actual_type env sigma cj tj.utj_val in
             sigma
         in
-        judge_of_case env sigma ci pj iv cj lfj
+        judge_of_case env sigma case ci pj iv cj lfj
 
     | Fix ((vn,i as vni),recdef) ->
         let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in
-- 
cgit v1.2.3


From 868b948f8a7bd583d467c5d02dfb34d328d53d37 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 11 Dec 2020 13:20:54 +0100
Subject: Remove redundant univ and parameter info from CaseInvert

---
 pretyping/typing.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index b0ce4fd63a..5b8b367ff2 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -391,8 +391,9 @@ let rec execute env sigma cstr =
         let sigma, lfj = execute_array env sigma lf in
         let sigma = match iv with
           | NoInvert -> sigma
-          | CaseInvert {univs;args} ->
-            let t = mkApp (mkIndU (ci.ci_ind,univs), args) in
+          | CaseInvert {indices} ->
+            let args = Array.append pms indices in
+            let t = mkApp (mkIndU (ci.ci_ind,u), args) in
             let sigma, tj = execute env sigma t in
             let sigma, tj = type_judgment env sigma tj in
             let sigma = check_actual_type env sigma cj tj.utj_val in
-- 
cgit v1.2.3