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/reductionops.mli | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'pretyping/reductionops.mli')

diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index ae93eb48b4..e60def72f6 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -57,9 +57,12 @@ module Stack : sig
 
   val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
 
+  type 'a case_stk =
+    case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array
+
   type 'a member =
   | App of 'a app_node
-  | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array
+  | Case of 'a case_stk
   | Proj of Projection.t
   | Fix of ('a, 'a) pfixpoint * 'a t
   | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red
-- 
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/reductionops.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/reductionops.mli')

diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index e60def72f6..59bc4a8b72 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -58,7 +58,7 @@ module Stack : sig
   val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
 
   type 'a case_stk =
-    case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array
+    case_info * EInstance.t * 'a array * 'a pcase_return * 'a pcase_invert * 'a pcase_branch array
 
   type 'a member =
   | App of 'a app_node
-- 
cgit v1.2.3