Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg

5 files changed, 34 insertions, 28 deletions

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
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 1a1560e5..55fababd 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -50,9 +50,12 @@ val print_universes : bool ref
 val print_no_symbol : bool ref
 val print_projections : bool ref
 
-(** Debug printing options *)
-val set_debug_global_reference_printer :
-  (loc -> global_reference -> reference) -> unit
+(** Customization of the global_reference printer *)
+val set_extern_reference :
+  (loc -> Idset.t -> global_reference -> reference) -> unit
+val get_extern_reference :
+  unit -> (loc -> Idset.t -> global_reference -> reference)
+
 val in_debugger : bool ref
 
 (** This governs printing of implicit arguments. If [with_implicits] is
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 81e4501a..e806686a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -650,7 +650,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
 	let scopes = find_arguments_scope ref in
 	Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
 	GRef (loc, ref), impls, scopes, []
-      with _ ->
+      with e when Errors.noncritical e ->
 	(* [id] a goal variable *)
 	GVar (loc,id), [], [], []
 
@@ -716,7 +716,7 @@ let intern_applied_reference intern env namedctx lvar args = function
       try
 	let r,args2 = intern_non_secvar_qualid loc qid intern env lvar args in
 	find_appl_head_data r, args2
-      with e ->
+      with e when Errors.noncritical e ->
 	(* Extra allowance for non globalizing functions *)
 	if !interning_grammar || env.unb then
 	  (GVar (loc,id), [], [], []),args
@@ -969,15 +969,15 @@ let sort_fields mode loc l completer =
 		    | [] -> anomaly "Number of projections mismatch"
 		    | (_, regular)::tm ->
 		       let boolean = not regular in
-		       if ConstRef name = global_reference_of_reference refer
-		       then
+                       (match global_reference_of_reference refer with
+                       | ConstRef name' when eq_constant name name' ->
 			 if boolean && mode then
 			   user_err_loc (loc, "", str"No local fields allowed in a record construction.")
 			 else build_patt b tm (i + 1) (i, snd acc) (* we found it *)
-		       else
+                       | _ ->
 			  build_patt b tm (if boolean&&mode then i else i + 1)
 			    (if boolean && mode then acc
-			     else fst acc, (i, ConstRef name) :: snd acc))
+			     else fst acc, (i, ConstRef name) :: snd acc)))
 	      | None :: b-> (* we don't want anonymous fields *)
 		 if mode then
 		   user_err_loc (loc, "", str "This record contains anonymous fields.")
@@ -1009,7 +1009,7 @@ let sort_fields mode loc l completer =
 			 (loc, "",
 			  str "This record contains fields of different records.")
 		   | (i, a) :: b->
-		       if glob_refer = a
+		       if eq_gr glob_refer a
 		       then (i,List.rev_append acc l)
 		       else add_patt b ((i,a)::acc)
 	         in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 9950178c..2c000258 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -88,8 +88,8 @@ let is_freevar ids env x =
     if Idset.mem x ids then false
     else
       try ignore(Environ.lookup_named x env) ; false
-      with _ -> not (is_global x)
-  with _ -> true
+      with e when Errors.noncritical e -> not (is_global x)
+  with e when Errors.noncritical e -> true
 
 (* Auxiliary functions for the inference of implicitly quantified variables. *)
 
diff --git a/interp/notation.ml b/interp/notation.ml
index e3fb5d5e..03fa23a3 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -838,4 +838,4 @@ let _ =
 let with_notation_protection f x =
   let fs = freeze () in
   try let a = f x in unfreeze fs; a
-  with e -> unfreeze fs; raise e
+  with reraise -> unfreeze fs; raise reraise