From 5eae5b130f87aabdfee23bbc9f4114fb5c0624b1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 14 Apr 2008 22:34:19 +0000
Subject: 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
---
 interp/constrextern.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'interp/constrextern.mli')

diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 7ae2977f5c..a56923fe5f 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
-- 
cgit v1.2.3