Diverses corrections

- gestion des idents (suite commit 10785) [lib, interp, contrib/ring, dev]
- suppression (enfin) des $id dans les constr (utilisation des MetaIdArg des
  quotations de tactiques pour simuler les métas des constr - quitte à devoir
  utiliser un let-in dans l'expression de tactique) [proofs, parsing, tactics]
- utilisation de error en place d'un "print_string" d'échec dans fourier
- améliorations espérées vis à vis de quelques "bizarreries" dans la gestion
  des Meta [pretyping]



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

2 files changed, 9 insertions, 26 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 1e3587c59..5047d1b98 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -108,35 +108,17 @@ let idopt_of_name = function
 let extern_evar loc n l =
   if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None)
 
-let rawdebug = ref false
-
-let raw_string_of_ref = function
-  | ConstRef kn -> 
-      "CONST("^(string_of_con kn)^")"
-  | IndRef (kn,i) ->
-      "IND("^(string_of_kn kn)^","^(string_of_int i)^")"
-  | ConstructRef ((kn,i),j) -> 
-      "CONSTRUCT("^
-      (string_of_kn kn)^","^(string_of_int i)^","^(string_of_int j)^")"
-  | VarRef id -> 
-      "SECVAR("^(string_of_id id)^")"
-
-let short_string_of_ref = function
-  | VarRef id -> string_of_id id
-  | ConstRef cst -> string_of_label (pi3 (repr_con cst))
-  | IndRef (kn,0) -> string_of_label (pi3 (repr_kn kn))
-  | IndRef (kn,i) -> 
-      "IND("^string_of_label (pi3 (repr_kn kn))^(string_of_int i)^")"
-  | ConstructRef ((kn,i),j) -> 
-      "CONSTRUCT("^
-      string_of_label (pi3 (repr_kn kn))^","^(string_of_int i)^","^(string_of_int j)^")"
+let debug_global_reference_printer =
+  ref (fun _ -> failwith "Cannot print a global reference")
+
+let set_debug_global_reference_printer f =
+  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 *)
-    let f = if !rawdebug then raw_string_of_ref else short_string_of_ref in
-    Ident (loc,id_of_string (f r))
+    !debug_global_reference_printer loc r
 
 (************************************************************************)
 (* Equality up to location (useful for translator v8) *)
@@ -922,7 +904,7 @@ let rec raw_of_pat env = function
 	| Name id   -> id
 	| Anonymous ->
 	    anomaly "rawconstr_of_pattern: index to an anonymous variable"
-      with Not_found -> id_of_string ("_UNBOUND_REL_"^(string_of_int n)^"]") in
+      with Not_found -> id_of_string ("_UNBOUND_REL_"^(string_of_int n)) in
       RVar (loc,id)
   | PMeta None -> RHole (loc,Evd.InternalHole)
   | PMeta (Some n) -> RPatVar (loc,(false,n))
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 7ae2977f5..a56923fe5 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -56,7 +56,8 @@ val print_no_symbol : bool ref
 val print_projections : bool ref
 
 (* Debug printing options *)
-val rawdebug : bool ref
+val set_debug_global_reference_printer :
+  (loc -> global_reference -> reference) -> unit
 
 (* This governs printing of implicit arguments. If [with_implicits] is
    on and not [with_arguments] then implicit args are printed prefixed