diff options
| author | Pierre-Marie Pédrot | 2019-02-04 13:19:34 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 13:19:34 +0100 |
| commit | 127f1fe146264a87d7a8cb04ab8ea34201b5c93a (patch) | |
| tree | 941b44ef3191544916f587de76f574d91545a7cb /pretyping | |
| parent | 129d47518ae950c6ef1b69763e93cd70c14863f6 (diff) | |
| parent | 25aaa4c5e9da90af41629d574dbc905f3781acd2 (diff) | |
Merge PR #9368: Discard argument names of section variables on section close
Reviewed-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/arguments_renaming.ml | 2 |
1 files changed, 1 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 |