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.

1 files changed, 4 insertions, 13 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 0f4651e26..2f8e5b964 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -284,7 +284,6 @@ sig
   | Proj of int * int * projection * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Cst of cst_member * int * int list * 'a t * Cst_stack.t
-  | Update of 'a
   and 'a t = 'a member list
 
   exception IncompatibleFold2
@@ -342,7 +341,6 @@ struct
   | Proj of int * int * projection * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Cst of cst_member * int * int list * 'a t * Cst_stack.t
-  | Update of 'a
   and 'a t = 'a member list
 
   let rec pr_member pr_c member =
@@ -365,7 +363,6 @@ struct
       ++ pr_comma () ++
 	prlist_with_sep pr_semicolon int remains ++
 	pr_comma () ++ pr pr_c params ++ str ")"
-    | Update t -> str "ZUpdate(" ++ pr_c t ++ str ")"
   and pr pr_c l =
     let open Pp in
     prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l
@@ -411,7 +408,6 @@ struct
     let rec equal_rec sk1 lft1 sk2 lft2  =
       match sk1,sk2 with
       | [],[] -> Some (lft1,lft2)
-      | (Update _ :: _, _ | _, Update _ :: _) -> assert false
       | App a1 :: s1, App a2 :: s2 ->
 	let t1,s1' = decomp_node_last a1 s1 in
 	let t2,s2' = decomp_node_last a2 s2 in
@@ -444,8 +440,6 @@ struct
     let rec compare_rec bal stk1 stk2 =
       match (stk1,stk2) with
 	([],[]) -> Int.equal bal 0
-      | ((Update _)::s1, _) -> compare_rec bal s1 stk2
-      | (_, (Update _)::s2) -> compare_rec bal stk1 s2
       | (App (i,_,j)::s1, _) -> compare_rec (bal + j + 1 - i) s1 stk2
       | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2
       | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) ->
@@ -486,12 +480,11 @@ struct
 	let (o',lft1',lft2') =
 	  aux o lft1 (List.rev params1) lft2 (List.rev params2)
 	in aux o' lft1' q1 lft2' q2
-      | (((Update _|App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) ->
+      | (((App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) ->
 	raise IncompatibleFold2
     in aux o 0 (List.rev sk1) 0 (List.rev sk2)
 
   let rec map f x = List.map (function
-			       | Update _ -> assert false
                                | (Proj (_,_,_,_)) as e -> e
 			       | App (i,a,j) ->
 				  let le = j - i + 1 in
@@ -509,7 +502,6 @@ struct
 
   let rec args_size = function
     | App (i,_,j)::s -> j + 1 - i + args_size s
-    | Update(_)::s -> args_size s
     | (Case _|Fix _|Proj _|Cst _)::_ | [] -> 0
 
   let strip_app s =
@@ -617,7 +609,6 @@ struct
   | f, (Proj (n,m,p,cst_l)::s) when refold ->
     zip (best_state sigma (mkProj (p,f),s) cst_l)
   | f, (Proj (n,m,p,_)::s) -> zip (mkProj (p,f),s)
-  | _, (Update _::_) -> assert false
   in
   zip s
 
@@ -1060,7 +1051,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 		(arg,
 		 Stack.Cst (const,next,remains',s' @ (Stack.append_app [|x'|] bef),cst_l) :: s''')
 	  end
-        |_, (Stack.App _|Stack.Update _)::_ -> assert false
+        |_, (Stack.App _)::_ -> assert false
 	|_, _ -> fold ()
       else fold ()
 
@@ -1141,7 +1132,7 @@ let local_whd_state_gen flags sigma =
 	|args, (Stack.Fix (f,s',cst)::s'') when use_fix ->
 	  let x' = Stack.zip sigma (x,args) in
 	  whrec (contract_fix sigma f, s' @ (Stack.append_app [|x'|] s''))
-        |_, (Stack.App _|Stack.Update _|Stack.Cst _)::_ -> assert false
+        |_, (Stack.App _|Stack.Cst _)::_ -> assert false
 	|_, _ -> s
       else s
 
@@ -1671,7 +1662,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
 	if isConstruct sigma t_o then
 	  whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'')
 	else s,csts'
-      |_, ((Stack.App _|Stack.Update _|Stack.Cst _) :: _|[]) -> s,csts'
+      |_, ((Stack.App _|Stack.Cst _) :: _|[]) -> s,csts'
   in whrec csts s
 
 let find_conclusion env sigma =