Printing bugs with match patterns:

- namegen.ml: if a matching variable has the same name as a constructor,
  rename it, even if the conflicting constructor name is defined in a
  different module;
- constrextern.ml: protect code for printing cases as terms are from
  requesting info in the global env when printers are called from ocamldebug
  since the global env is undefined in this situation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14947 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 15 insertions, 8 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index be60c9c30..bd8e78c0f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -140,14 +140,19 @@ let extern_evar loc n l =
 let debug_global_reference_printer =
   ref (fun _ -> failwith "Cannot print a global reference")
 
+let in_debugger = ref false
+
 let set_debug_global_reference_printer f =
+  in_debugger := true;
   debug_global_reference_printer := f
 
 let extern_reference loc vars r =
-  try Qualid (loc,shortest_qualid_of_global vars r)
-  with Not_found ->
-    (* happens in debugger *)
+  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)
+
 
 (************************************************************************)
 (* Equality up to location (useful for translator v8) *)
@@ -371,7 +376,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	  let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
 	  let p =
 	    try
-              if !Flags.raw_print then raise Exit;
+              if !in_debugger || !Flags.raw_print then raise Exit;
 	      let projs = Recordops.lookup_projections (fst cstrsp) in
 	      let rec ip projs args acc =
 		match projs with
@@ -388,15 +393,17 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	      CPatRecord(loc, List.rev (ip projs args []))
 	    with
 		Not_found | No_match | Exit ->
+                  let c = extern_reference loc Idset.empty (ConstructRef cstrsp) in
+                  if !in_debugger then CPatCstr (loc, c, args) else
 		  if !Topconstr.oldfashion_patterns then
 		    if pattern_printable_in_both_syntax cstrsp
-		    then CPatCstr (loc, extern_reference loc vars (ConstructRef cstrsp), args)
-		    else CPatCstrExpl (loc, extern_reference loc vars (ConstructRef cstrsp), add_patt_for_params cstrsp args)
+		    then CPatCstr (loc, c, args)
+		    else CPatCstrExpl (loc, c, add_patt_for_params cstrsp args)
 		  else
 		    let full_args = add_patt_for_params cstrsp args in
 		    match drop_implicits_in_patt cstrsp full_args with
-		      |Some true_args -> CPatCstr (loc, extern_reference loc vars (ConstructRef cstrsp), true_args)
-		      |None -> CPatCstrExpl (loc, extern_reference loc vars (ConstructRef cstrsp), full_args)
+		      |Some true_args -> CPatCstr (loc, c, true_args)
+		      |None -> CPatCstrExpl (loc, c, full_args)
 	  in insert_pat_alias loc p na
 
 and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function