diff options
Diffstat (limited to 'tactics/declare.ml')
| -rw-r--r-- | tactics/declare.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index 324007930a..5135d72f7b 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -93,13 +93,14 @@ let load_constant i ((sp,kn), obj) = Dumpglob.add_constant_kind con obj.cst_kind (* Opening means making the name without its module qualification available *) -let open_constant i ((sp,kn), obj) = +let open_constant f i ((sp,kn), obj) = (* Never open a local definition *) match obj.cst_locl with | ImportNeedQualified -> () | ImportDefaultBehavior -> let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con) + if in_filter_ref (GlobRef.ConstRef con) f then + Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con) let exists_name id = Decls.variable_exists id || Global.exists_objlabel (Label.of_id id) |