diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-08-10 11:59:45 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-08-10 11:59:45 +0200 |
| commit | 5f7463e1ad99f530e078ecbc600347328d603bb4 (patch) | |
| tree | c5bfca90c4639047d0d14d5efa7c350a4bdc6dd5 /kernel/vconv.ml | |
| parent | 90303e38d22479105927f0dd2fe95cce9447bd44 (diff) | |
Make code a bit clearer by removing optional argument.
Diffstat (limited to 'kernel/vconv.ml')
| -rw-r--r-- | kernel/vconv.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml index c729a6ce2..894f5296a 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -116,14 +116,14 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = | Atype _ , _ | _, Atype _ -> assert false | Aind _, _ | Aid _, _ -> raise NotConvertible -and conv_stack env ?from:(from=0) k stk1 stk2 cu = +and conv_stack env k stk1 stk2 cu = match stk1, stk2 with | [], [] -> cu | Zapp args1 :: stk1, Zapp args2 :: stk2 -> - conv_stack env k stk1 stk2 (conv_arguments env ~from:from k args1 args2 cu) + conv_stack env k stk1 stk2 (conv_arguments env k args1 args2 cu) | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 -> conv_stack env k stk1 stk2 - (conv_arguments env ~from:from k args1 args2 (conv_fix env k f1 f2 cu)) + (conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu)) | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 -> if check_switch sw1 sw2 then let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in |