- Nouvelle option "Set Printing Existential Instances" pour forcer

  l'affichage des instances des evars.
- Nouveaux boutons "interrupteurs" pour activer/désactiver à volonté
  l'affichage des implicites, coercions, notations, etc dans CoqIDE
  (reste à trouver des icônes appropriées !).


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

1 files changed, 12 insertions, 0 deletions

diff --git a/ide/coq.mli b/ide/coq.mli
index 5ded2b573..cbc763df8 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -15,6 +15,18 @@ open Evd
 
 val version : unit -> string
 
+type printing_state = {
+  mutable printing_implicit : bool;
+  mutable printing_coercions : bool;
+  mutable printing_raw_matching : bool;
+  mutable printing_no_notation : bool;
+  mutable printing_all : bool;
+  mutable printing_evar_instances : bool;
+  mutable printing_universes : bool
+}
+
+val printing_state : printing_state
+
 type reset_mark =
   | ResetToId of Names.identifier
   | ResetToState of  Libnames.object_name