From 1db7a2ab06f866cc20c0f29eb8b82577034b5378 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 18 Apr 2013 08:48:15 +0000
Subject: Fix #3001 (rename arg of global cst inside section)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16426 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/arguments_renaming.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index b7ecb24617..42099f5dbb 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -49,12 +49,14 @@ let section_segment_of_reference = function
   | _ -> []
 
 let discharge_rename_args = function
-  | _, (ReqGlobal (c, names), _) ->
-     let c' = pop_global_reference c in
-     let vars = section_segment_of_reference c in
-     let var_names = List.map (fun (id, _,_,_) -> Name id) vars in
-     let names' = List.map (fun l -> var_names @ l) names in
-     Some (ReqGlobal (c', names), (c', names'))
+  | _, (ReqGlobal (c, names), _ as req) ->
+     (try 
+       let vars = section_segment_of_reference c in
+       let c' = pop_global_reference c in
+       let var_names = List.map (fun (id, _,_,_) -> Name id) vars in
+       let names' = List.map (fun l -> var_names @ l) names in
+       Some (ReqGlobal (c', names), (c', names'))
+     with Not_found -> Some req)
   | _ -> None
 
 let rebuild_rename_args x = x
-- 
cgit v1.2.3