From 8380c9f55f3ce5a62006e22d2c55aea70d4dfcac Mon Sep 17 00:00:00 2001
From: jnarboux
Date: Mon, 26 May 2008 16:21:31 +0000
Subject: remove set printing ... and unset printing ... from template menu as
 they are no useless in coqide

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10994 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coq_commands.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index fdaee4508e..12ef8db74a 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -109,9 +109,9 @@ let commands = [
      "Set Extraction Optimize";
      "Set Hyps__limit";
      "Set Implicit Arguments";
-     "Set Printing Coercion";
+     (*"Set Printing Coercion";
      "Set Printing Coercions";
-     "Set Printing Synth";
+     "Set Printing Synth";*)
      "Set Printing Wildcard";
      "Set Silent.";
      "Set Undo";
@@ -142,9 +142,10 @@ let commands = [
    "Unset Extraction Optimize";
    "Unset Hyps__limit";
    "Unset Implicit Arguments";
+   (*
    "Unset Printing Coercion";
    "Unset Printing Coercions";
-   "Unset Printing Synth";
+   "Unset Printing Synth"; *)
    "Unset Printing Wildcard";
    "Unset Silent.";
    "Unset Undo";];
-- 
cgit v1.2.3