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

(limited to 'pretyping/evarconv.ml')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 18e0c31dd6..a066e3c20b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -310,8 +310,7 @@ let ise_stack2 no_app env evd f sk1 sk2 =
         | Success i' -> ise_stack2 true i' q1 q2
         | UnifFailure _ as x -> fail x
       else fail (UnifFailure (i,NotSameHead))
-    | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _
-    | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false
+    | Stack.Update _ :: _, _ | _, Stack.Update _ :: _ -> assert false
     | Stack.App _ :: _, Stack.App _ :: _ ->
        if no_app && deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else
 	 begin match ise_app_stack2 env f i sk1 sk2 with
@@ -344,8 +343,7 @@ let exact_ise_stack2 env evd f sk1 sk2 =
        if Constant.equal (Projection.constant p1) (Projection.constant p2)
        then ise_stack2 i q1 q2
        else (UnifFailure (i, NotSameHead))
-    | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _
-    | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false
+    | Stack.Update _ :: _, _ | _, Stack.Update _ :: _-> assert false
     | Stack.App _ :: _, Stack.App _ :: _ ->
 	 begin match ise_app_stack2 env f i sk1 sk2 with
 	       |_,(UnifFailure _ as x) -> x
@@ -457,7 +455,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     let out1 = whd_betaiota_deltazeta_for_iota_state
       (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in
     let out2 = whd_nored_state evd
-      (Stack.zip evd (term', sk' @ [Stack.Shift 1]), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), 
+      (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty),
       Cst_stack.empty in
     if onleft then evar_eqappr_x ts env' evd CONV out1 out2
     else evar_eqappr_x ts env' evd CONV out2 out1
-- 
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/evarconv.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'pretyping/evarconv.ml')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index a066e3c20b..e5776d2eca 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -310,7 +310,6 @@ let ise_stack2 no_app env evd f sk1 sk2 =
         | Success i' -> ise_stack2 true i' q1 q2
         | UnifFailure _ as x -> fail x
       else fail (UnifFailure (i,NotSameHead))
-    | Stack.Update _ :: _, _ | _, Stack.Update _ :: _ -> assert false
     | Stack.App _ :: _, Stack.App _ :: _ ->
        if no_app && deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else
 	 begin match ise_app_stack2 env f i sk1 sk2 with
@@ -343,7 +342,6 @@ let exact_ise_stack2 env evd f sk1 sk2 =
        if Constant.equal (Projection.constant p1) (Projection.constant p2)
        then ise_stack2 i q1 q2
        else (UnifFailure (i, NotSameHead))
-    | Stack.Update _ :: _, _ | _, Stack.Update _ :: _-> assert false
     | Stack.App _ :: _, Stack.App _ :: _ ->
 	 begin match ise_app_stack2 env f i sk1 sk2 with
 	       |_,(UnifFailure _ as x) -> x
-- 
cgit v1.2.3