diff options
| -rw-r--r-- | interp/constrintern.ml | 22 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_13249.v | 9 |
2 files changed, 22 insertions, 9 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b86ad7175a..c7ed066f7e 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -534,15 +534,19 @@ let intern_generalized_binder intern_type ntnvars in let na = match na with | Anonymous -> - let name = - let id = - match ty with - | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid -> - qualid_basename qid - | _ -> default_non_dependent_ident - in Implicit_quantifiers.make_fresh ids' (Global.env ()) id - in Name name - | _ -> na in + let id = + match ty with + | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid -> + qualid_basename qid + | _ -> default_non_dependent_ident + in + let ids' = List.fold_left (fun ids' lid -> Id.Set.add lid.CAst.v ids') ids' fvs in + let id = + Implicit_quantifiers.make_fresh ids' (Global.env ()) id + in + Name id + | _ -> na + in let impls = impls_type_list 1 ty' in (push_name_env ntnvars impls env' (make ?loc na), (make ?loc (na,b',ty')) :: List.rev bl) diff --git a/test-suite/bugs/closed/bug_13249.v b/test-suite/bugs/closed/bug_13249.v new file mode 100644 index 0000000000..06f7ddbd3a --- /dev/null +++ b/test-suite/bugs/closed/bug_13249.v @@ -0,0 +1,9 @@ +Global Generalizable All Variables. + +Section test. + Context {A : Type}. + Context `{!foo A}. + + Goal foo A. + Proof. assumption. Defined. +End test. |