Imported Upstream version 8.4pl3dfsgupstream/8.4pl3dfsg

1 files changed, 8 insertions, 6 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index a145508a..92378837 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -56,12 +56,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