diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-08-31 16:53:16 +0200 |
|---|---|---|
| committer |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-07-03 13:36:05 +0200 |
| commit | 63dcea6edba9a71c5320b54e0efa64ddac01bb52 (patch) | |
| tree | 5df793ce8857b4c5f38483bb0c8d2d55eb6216bc /kernel | |
| parent | 5882858a15dbbfb53853ea8b3685bd44f43ae4ce (diff) | |
Subtyping.check_constant: remove unused module path argument.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/subtyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 1e58f5c24..74042f9e0 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -224,7 +224,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 cst -let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = +let check_constant cst env l info1 cb2 spec2 subst1 subst2 = let error why = error_signature_mismatch l spec2 why in let check_conv cst poly f = check_conv_error error cst poly f in let check_type poly cst env t1 t2 = @@ -292,7 +292,7 @@ and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= let check_one_body cst (l,spec2) = match spec2 with | SFBconst cb2 -> - check_constant cst env mp1 l (get_obj mp1 map1 l) + check_constant cst env l (get_obj mp1 map1 l) cb2 spec2 subst1 subst2 | SFBmind mib2 -> check_inductive cst env mp1 l (get_obj mp1 map1 l) |