Changing the commands to switch to textual explanation of proofs.

Removing the "Show Dad Rules." command that breaks down parsing.


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

1 files changed, 6 insertions, 8 deletions

diff --git a/contrib/interface/Centaur.v b/contrib/interface/Centaur.v
index ffd7d5b86..80142df4d 100644
--- a/contrib/interface/Centaur.v
+++ b/contrib/interface/Centaur.v
@@ -5,18 +5,14 @@ Declare ML Module "vtp".
 Declare ML Module "translate".
 Declare ML Module "pbp".
 Declare ML Module "dad".
-(*
-Declare ML Module "showproofutil".
 Declare ML Module "showproof_ct".
 Declare ML Module "showproof".
-Declare ML Module "fine_search".
-*)
 Declare ML Module "debug_tac".
 Declare ML Module "paths".
 Declare ML Module "history".
 Declare ML Module "centaur".
 (* Require Export Illustrations. *)
-Require Export AddDad.
+(* Require Export AddDad. *)
 
 Grammar vernac vernac : ast :=
   goal_cmd [ "Goal" "Cmd" numarg($n) "with" tacarg($tac) "." ] ->
@@ -35,7 +31,7 @@ Grammar vernac vernac : ast :=
 | compute_in_goal [ "COMPUTE_IN_GOAL" numarg($n) constrarg($c) "." ] ->
        [(CHECK_IN_GOAL "COMPUTE" $n $c)]
 | centaur_reset [ "Centaur" "Reset" identarg($id) "." ] -> [(Centaur_Reset $id)]
-| show_dad_rules [ "Show" "Dad" "Rules" "." ] -> [(Show_dad_rules)]
+(* | show_dad_rules [ "Show" "Dad" "Rules" "." ] -> [(Show_dad_rules)] *)
 | start_pcoq [ "Start" "Pcoq" "Mode" "." ] -> [ (START_PCOQ) ]
 | start_pcoq [ "Start" "Pcoq" "Debug" "Mode" "." ] -> [ (START_PCOQ_DEBUG) ].
 Grammar vernac ne_id_list : List :=
@@ -76,8 +72,10 @@ Grammar tactic simple_tactic : ast :=
    displayed with a readable syntax.  It is not sure, since the error reporting
    procedure changed from V6.1 and does not reprint the command anymore. *)
 Grammar vernac vernac : ast :=
-  text_proof_flag_on [ "Text" "Mode" "On" "." ] ->
-       [(TEXT_MODE (AST {on}))]
+  text_proof_flag_on [ "Text" "Mode" "fr" "." ] ->
+       [(TEXT_MODE (AST {fr}))]
+| text_proof_flag_on [ "Text" "Mode" "en" "." ] ->
+       [(TEXT_MODE (AST {en}))]
 | text_proof_flag_on [ "Text" "Mode" "Off" "." ] ->
        [(TEXT_MODE (AST {off}))].