From 866b449c497933a3ab1185c194d8d33a86c432f2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 6 Dec 2017 17:53:55 +0100
Subject: Getting rid of the Shift constructor in Reductionops.

It was actually not used. The only place generating one was easily writable
without it.
---
 pretyping/reductionops.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'pretyping/reductionops.mli')

diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index db0c29aeff..c6c55209e7 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -82,7 +82,6 @@ module Stack : sig
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *)
     * 'a t * Cst_stack.t
-  | Shift of int
   | Update of 'a
   and 'a t = 'a member list
 
@@ -107,7 +106,7 @@ module Stack : sig
   val append_app_list : 'a list -> 'a t -> 'a t
 
   (** if [strip_app s] = [(a,b)], then [s = a @ b] and [b] does not
-      start by App or Shift *)
+      start by App *)
   val strip_app : 'a t -> 'a t * 'a t
   (** @return (the nth first elements, the (n+1)th element, the remaining stack)  *)
   val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
-- 
cgit v1.2.3


From 7ced1ba0e6bf47efd75a4c7c607a99bc1198f4f3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 6 Dec 2017 18:02:56 +0100
Subject: Getting rid of the Update constructor in Reductionops.

This was dead code, probably due to the fact it was once shared with the
kernel stack type.
---
 pretyping/reductionops.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'pretyping/reductionops.mli')

diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index c6c55209e7..34fdbe8583 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -82,7 +82,6 @@ module Stack : sig
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *)
     * 'a t * Cst_stack.t
-  | Update of 'a
   and 'a t = 'a member list
 
   val pr : ('a -> Pp.t) -> 'a t -> Pp.t
-- 
cgit v1.2.3