diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 13 |
1 files changed, 2 insertions, 11 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e71daef999..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 @@ -481,7 +472,7 @@ let explicitize loc inctx impl (cf,f) args = (!print_implicits && !print_implicits_explicit_args) || (is_needed_for_correct_partial_application tail imp) || (!print_implicits_defensive && - (not (is_inferable_implicit inctx n imp) || !Flags.beautify_file) && + (not (is_inferable_implicit inctx n imp) || !Flags.beautify) && is_significant_implicit (Lazy.force a)) in if visible then |