diff options
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 |