diff options
author | Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
commit | d2c5c5e616a6e118291fe1ce9965c731adac03a8 (patch) | |
tree | 7b000ad50dcc45ff1c63768a983cded1e23a07ca /pretyping/arguments_renaming.ml | |
parent | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (diff) |
Imported Upstream version 8.4pl3dfsgupstream/8.4pl3dfsg
Diffstat (limited to 'pretyping/arguments_renaming.ml')
-rw-r--r-- | pretyping/arguments_renaming.ml | 14 |
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 |