diff options
| author | Gaetan Gilbert | 2017-04-25 14:31:15 +0200 |
|---|---|---|
| committer | Gaetan Gilbert | 2017-04-27 21:42:01 +0200 |
| commit | 87910d7be9bd50de4db80f70c6e287c7c7994460 (patch) | |
| tree | ff0c9daa7ff73f0eb19e8b62ea6f689b154f314b /pretyping/reductionops.ml | |
| parent | 5eb09af1e3686d6ac518b9eafe7cfcebd2b16375 (diff) | |
Fix 4.04 warnings
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 da3add2e5a..52f424f751 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 |
