diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 17 |
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 = |