diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-01-26 16:56:33 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-01-26 16:56:33 +0100 |
commit | 164c6861860e6b52818c031f901ffeff91fca16a (patch) | |
tree | 4f91d20c890c25915e7b28226c663b94a8cfb0d3 /interp/constrextern.ml | |
parent | 91dbeab8eef959c3f64960909ca69d4e68c8198d (diff) |
Imported Upstream version 8.5upstream/8.5
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 |