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 /checker | |
| parent | 5882858a15dbbfb53853ea8b3685bd44f43ae4ce (diff) | |
Subtyping.check_constant: remove unused module path argument.
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/subtyping.ml | 4 |
1 files changed, 2 insertions, 2 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) |