diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-13 15:21:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-23 18:50:10 +0200 |
| commit | 944f62d08b7d78bcb20dd12ba138891d432b5987 (patch) | |
| tree | 85f69d1898ea3704cf43e6f03b49f5426d7f9f2a /kernel/reduction.ml | |
| parent | f2ab2825077bf8344d2e55be433efb1891212589 (diff) | |
Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 81fbd4f5e..38106fbf6 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -84,7 +84,7 @@ let map_lift (l : lift) (v : fconstr array) = match v with | [|c0; c1|] -> [|(l, c0); (l, c1)|] | [|c0; c1; c2|] -> [|(l, c0); (l, c1); (l, c2)|] | [|c0; c1; c2; c3|] -> [|(l, c0); (l, c1); (l, c2); (l, c3)|] -| v -> CArray.Fun1.map (fun l t -> (l, t)) l v +| v -> Array.Fun1.map (fun l t -> (l, t)) l v let pure_stack lfts stk = let rec pure_rec lfts stk = |