diff options
| author | Pierre-Marie Pédrot | 2015-11-29 19:05:53 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-11-29 19:13:30 +0100 |
| commit | e98d3c3793f26265a49f63a6e78d704f88341df9 (patch) | |
| tree | c0328afc0034f3262dca2ca067531ee19bbb0ee0 /interp | |
| parent | 103ec7205d9038f1f3821f9287e3bb0907a1e3ec (diff) | |
| parent | 8d6e58e16cc53a3198eb4c4afef0a2c39f6a5c56 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f57772ecb0..5160f07af0 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -147,8 +147,17 @@ let extern_evar loc n l = CEvar (loc,n,l) For instance, in the debugger the tables of global references may be inaccurate *) +let safe_shortest_qualid_of_global vars r = + try shortest_qualid_of_global vars r + with Not_found -> + match r with + | VarRef v -> make_qualid DirPath.empty v + | ConstRef c -> make_qualid DirPath.empty Names.(Label.to_id (con_label c)) + | IndRef (i,_) | ConstructRef ((i,_),_) -> + make_qualid DirPath.empty Names.(Label.to_id (mind_label i)) + let default_extern_reference loc vars r = - Qualid (loc,shortest_qualid_of_global vars r) + Qualid (loc,safe_shortest_qualid_of_global vars r) let my_extern_reference = ref default_extern_reference |