From 25aaa4c5e9da90af41629d574dbc905f3781acd2 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Sun, 20 Jan 2019 19:22:09 -0800
Subject: Discard argument names of section variables on section close

---
 pretyping/arguments_renaming.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3