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

1 files changed, 8 insertions, 6 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index b7ecb2461..42099f5db 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