diff options
Diffstat (limited to 'contrib/interface/Centaur.v')
| -rw-r--r-- | contrib/interface/Centaur.v | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/contrib/interface/Centaur.v b/contrib/interface/Centaur.v index ffd7d5b86a..80142df4d0 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}))]. |