diff options
| author | Pierre-Marie Pédrot | 2018-10-06 13:55:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-06 13:55:48 +0200 |
| commit | 371566f7619aed79aad55ffed6ee0920b961be6e (patch) | |
| tree | f5a7f56d5d5e924987ef0970aa0b72ec53aad673 /kernel/modops.ml | |
| parent | 28df7dd06dbea299736f3897ecabd2a6e3fd8e28 (diff) | |
| parent | 650c65af484c45f4e480252b55d148bcc198be6c (diff) | |
Merge PR #8555: Remove section paths from kernel names
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 424d329e09..bab2eae3df 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -289,10 +289,10 @@ let add_retroknowledge = let rec add_structure mp sign resolver linkinfo env = let add_one env (l,elem) = match elem with |SFBconst cb -> - let c = constant_of_delta_kn resolver (KerName.make2 mp l) in + let c = constant_of_delta_kn resolver (KerName.make mp l) in Environ.add_constant_key c cb linkinfo env |SFBmind mib -> - let mind = mind_of_delta_kn resolver (KerName.make2 mp l) in + let mind = mind_of_delta_kn resolver (KerName.make mp l) in let mib = if mib.mind_private != None then { mib with mind_private = Some true } @@ -331,7 +331,7 @@ let strengthen_const mp_from l cb resolver = match cb.const_body with |Def _ -> cb |_ -> - let kn = KerName.make2 mp_from l in + let kn = KerName.make mp_from l in let con = constant_of_delta_kn resolver kn in let u = match cb.const_universes with @@ -450,8 +450,8 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso = (* If we are performing an inclusion we need to add the fact that the constant mp_to.l is \Delta-equivalent to reso(mp_from.l) *) - let kn_from = KerName.make2 mp_from l in - let kn_to = KerName.make2 mp_to l in + let kn_from = KerName.make mp_from l in + let kn_to = KerName.make mp_to l in let old_name = kn_of_delta reso kn_from in add_kn_delta_resolver kn_to old_name reso', str' else @@ -471,8 +471,8 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso = in (* Same as constant *) if incl then - let kn_from = KerName.make2 mp_from l in - let kn_to = KerName.make2 mp_to l in + let kn_from = KerName.make mp_from l in + let kn_to = KerName.make mp_to l in let old_name = kn_of_delta reso kn_from in add_kn_delta_resolver kn_to old_name reso', str' else |