diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index da3add2e5..52f424f75 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -239,6 +239,9 @@ sig | Shift of int | Update of 'a and 'a t = 'a member list + + exception IncompatibleFold2 + val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds val empty : 'a t val is_empty : 'a t -> bool @@ -413,6 +416,7 @@ struct | (_,_) -> false in compare_rec 0 stk1 stk2 + exception IncompatibleFold2 let fold2 f o sk1 sk2 = let rec aux o lft1 sk1 lft2 sk2 = let fold_array = @@ -442,7 +446,7 @@ struct aux o lft1 (List.rev params1) lft2 (List.rev params2) in aux o' lft1' q1 lft2' q2 | (((Update _|App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) -> - raise (Invalid_argument "Reductionops.Stack.fold2") + raise IncompatibleFold2 in aux o 0 (List.rev sk1) 0 (List.rev sk2) let rec map f x = List.map (function |