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 | |
| parent | 5882858a15dbbfb53853ea8b3685bd44f43ae4ce (diff) | |
Subtyping.check_constant: remove unused module path argument.
| -rw-r--r-- | checker/subtyping.ml | 4 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 6d0d6f6c6..3f7f84470 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -217,7 +217,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= let _ = Array.map2_i check_cons_types mib1.mind_packets mib2.mind_packets in () -let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = +let check_constant env l info1 cb2 spec2 subst1 subst2 = let error () = error_not_match l spec2 in let check_conv f = check_conv_error error f in let check_type env t1 t2 = check_conv conv_leq env t1 t2 in @@ -281,7 +281,7 @@ and check_signatures env mp1 sig1 sig2 subst1 subst2 = let check_one_body (l,spec2) = match spec2 with | SFBconst cb2 -> - check_constant env mp1 l (get_obj mp1 map1 l) + check_constant env l (get_obj mp1 map1 l) cb2 spec2 subst1 subst2 | SFBmind mib2 -> check_inductive env mp1 l (get_obj mp1 map1 l) 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) |