diff options
| author | Jasper Hugunin | 2019-01-20 19:22:09 -0800 |
|---|---|---|
| committer | Jasper Hugunin | 2019-01-20 19:22:09 -0800 |
| commit | 25aaa4c5e9da90af41629d574dbc905f3781acd2 (patch) | |
| tree | 784abe20cdf3bd408f067122027d87b7ea8d9ea8 | |
| parent | 051b6efe1d730afe1a08eecac71282e24c4d4523 (diff) | |
Discard argument names of section variables on section close
| -rw-r--r-- | pretyping/arguments_renaming.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_9367.v | 12 |
2 files changed, 13 insertions, 1 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 0ace11839e..08df9a2460 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -43,7 +43,7 @@ let subst_rename_args (subst, (_, (r, names as orig))) = if r==r' then orig else (r', names) let discharge_rename_args = function - | _, (ReqGlobal (c, names), _ as req) -> + | _, (ReqGlobal (c, names), _ as req) when not (isVarRef c && Lib.is_in_section c) -> (try let vars = Lib.variable_section_segment_of_reference c in let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in diff --git a/test-suite/bugs/closed/bug_9367.v b/test-suite/bugs/closed/bug_9367.v new file mode 100644 index 0000000000..885f6bc391 --- /dev/null +++ b/test-suite/bugs/closed/bug_9367.v @@ -0,0 +1,12 @@ +Section foo. +Variable f : forall n : nat, nat. +Arguments f {_}. +Check f (n := 3). +Global Arguments f {bar} : rename. +End foo. + +Section foo. +Variable f : forall n : nat, nat. +Arguments f {_}. +Fail Check f (bar := 3). +End foo. |