From 50f832729dd03e7395e39a7ae2bd9cd1455c006e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 16 Oct 2003 15:03:28 +0000
Subject: Debranchement de l'affichage systematique des projections avec la
 notation pointee; soumis maintenant a l'activation de l'option 'Set Printing
 Projections'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4651 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrextern.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index d088867c54..b821b63fe8 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -43,13 +43,14 @@ val extern_constr : bool -> env -> constr -> constr_expr
 val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr
 val extern_reference : loc -> Idset.t -> global_reference -> reference
 
-(* For debugging *)
+(* Printing options *)
 val print_implicits : bool ref
 val print_arguments : bool ref
 val print_evar_arguments : bool ref
 val print_coercions : bool ref
 val print_universes : bool ref
 val print_no_symbol : bool ref
+val print_projections : bool ref
 
 (* 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