From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 8 May 2013 17:47:10 +0200
Subject: Imported Upstream version 8.4pl2dfsg

---
 interp/constrextern.ml | 33 ++++++++++++++++++---------------
 1 file changed, 18 insertions(+), 15 deletions(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 20b9c2a3..ee529fe0 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -137,20 +137,21 @@ let insert_pat_alias loc p = function
 let extern_evar loc n l =
   if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None)
 
-let debug_global_reference_printer =
-  ref (fun _ -> failwith "Cannot print a global reference")
+(** We allow customization of the global_reference printer.
+    For instance, in the debugger the tables of global references
+    may be inaccurate *)
 
-let in_debugger = ref false
+let default_extern_reference loc vars r =
+  Qualid (loc,shortest_qualid_of_global vars r)
 
-let set_debug_global_reference_printer f =
-  debug_global_reference_printer := f
+let my_extern_reference = ref default_extern_reference
 
-let extern_reference loc vars r =
-  if !in_debugger then
-    (* Debugger does not have the tables of global reference at hand *)
-    !debug_global_reference_printer loc r
-  else
-    Qualid (loc,shortest_qualid_of_global vars r)
+let set_extern_reference f = my_extern_reference := f
+let get_extern_reference () = !my_extern_reference
+
+let extern_reference loc vars l = !my_extern_reference loc vars l
+
+let in_debugger = ref false
 
 
 (************************************************************************)
@@ -303,10 +304,10 @@ let make_notation_gen loc ntn mknot mkprim destprim l =
 	match decompose_notation_key ntn, l with
 	| [Terminal "-"; Terminal x], [] ->
 	    (try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x)))
-	     with _ -> mknot (loc,ntn,[]))
+	     with e when Errors.noncritical e -> mknot (loc,ntn,[]))
 	| [Terminal x], [] ->
 	    (try mkprim (loc, Numeral (Bigint.of_string x))
-	     with _ -> mknot (loc,ntn,[]))
+	     with e when Errors.noncritical e -> mknot (loc,ntn,[]))
 	| _ ->
 	    mknot (loc,ntn,l)
 
@@ -816,12 +817,14 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
                 match f with
                 | GRef (_,ref) ->
 	          let subscopes =
-		    try list_skipn n (find_arguments_scope ref) with _ -> [] in
+		    try list_skipn n (find_arguments_scope ref)
+                    with e when Errors.noncritical e -> [] in
 	          let impls =
 		    let impls =
 		      select_impargs_size
 		        (List.length args) (implicits_of_global ref) in
-		    try list_skipn n impls with _ -> [] in
+		    try list_skipn n impls
+                    with e when Errors.noncritical e -> [] in
                   subscopes,impls
                 | _ ->
                   [], [] in
-- 
cgit v1.2.3