diff options
| author | Pierre-Marie Pédrot | 2016-10-17 13:53:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-10-17 13:53:35 +0200 |
| commit | 8adcc8d26a200a5e52cf0413b6672aa63f9d6ea2 (patch) | |
| tree | 11ebb0a691e61aa235257ef750875abc908b3c4c /interp | |
| parent | e5f8038f82c8a444afcfb7333a4c690b005fcff6 (diff) | |
| parent | 159b10655172b6f0888f9622be3620c3c33d35b1 (diff) | |
Merge PR #310 into v8.6
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index afc1c4caf8..dd8a48b85e 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -149,17 +149,8 @@ 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,safe_shortest_qualid_of_global vars r) + Qualid (loc,shortest_qualid_of_global vars r) let my_extern_reference = ref default_extern_reference |