diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f57772ec..9df8f9c2 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 @@ -438,8 +447,8 @@ let is_projection nargs = function | Some r when not !Flags.in_debugger && not !Flags.raw_print && !print_projections -> (try let n = Recordops.find_projection_nparams r + 1 in - if n <= nargs then None - else Some n + if n <= nargs then Some n + else None with Not_found -> None) | _ -> None |