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

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index bd875cf68b..04feae35d8 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -356,8 +356,7 @@ let make_case_or_project env sigma indt ci pred c branches =
   let IndType (((ind,_),_),_) = indt in
   let projs = get_projections env ind in
   match projs with
-  | None ->
-    mkCase (ci, pred, make_case_invert env indt ci, c, branches)
+  | None -> (mkCase (EConstr.contract_case env sigma (ci, pred, make_case_invert env indt ci, c, branches)))
   | Some ps ->
      assert(Array.length branches == 1);
      let na, ty, t = destLambda sigma pred in
@@ -749,6 +748,6 @@ let control_only_guard env sigma c =
   in
   let rec iter env c =
     check_fix_cofix env c;
-    EConstr.iter_with_full_binders sigma EConstr.push_rel iter env c
+    EConstr.iter_with_full_binders env sigma EConstr.push_rel iter env c
   in
   iter env c
-- 
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/inductiveops.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 04feae35d8..d02b015604 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -344,11 +344,7 @@ let get_projections = Environ.get_projections
 
 let make_case_invert env (IndType (((ind,u),params),indices)) ci =
   if Typeops.should_invert_case env ci
-  then
-    let univs = EConstr.EInstance.make u in
-    let params = Array.map_of_list EConstr.of_constr params in
-    let args = Array.append params (Array.of_list indices) in
-    CaseInvert {univs;args}
+  then CaseInvert {indices=Array.of_list indices}
   else NoInvert
 
 let make_case_or_project env sigma indt ci pred c branches =
-- 
cgit v1.2.3