streamlines the keywords for definitions, require commandsbinders, notation

definitions, Show commands, Print commands, proof starting commands,
Search commands, scope commands, type reservation command, locate commands,
time


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

3 files changed, 397 insertions, 168 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index e99392ccb..e50d1a1f6 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -1,9 +1,4 @@
-type ct_ASSOC =
-    CT_coerce_NONE_to_ASSOC of ct_NONE
-  | CT_lefta
-  | CT_nona
-  | CT_righta
-and ct_AST =
+type ct_AST =
     CT_coerce_ID_OR_INT_to_AST of ct_ID_OR_INT
   | CT_coerce_ID_OR_STRING_to_AST of ct_ID_OR_STRING
   | CT_astnode of ct_ID * ct_AST_LIST
@@ -16,6 +11,7 @@ and ct_BINARY =
 and ct_BINDER =
     CT_coerce_DEF_to_BINDER of ct_DEF
   | CT_binder of ct_ID_OPT_NE_LIST * ct_FORMULA
+  | CT_binder_coercion of ct_ID_OPT_NE_LIST * ct_FORMULA
 and ct_BINDER_LIST =
     CT_binder_list of ct_BINDER list
 and ct_BINDER_NE_LIST =
@@ -45,26 +41,31 @@ and ct_COFIX_TAC_LIST =
 and ct_COMMAND =
     CT_coerce_COMMAND_LIST_to_COMMAND of ct_COMMAND_LIST
   | CT_coerce_EVAL_CMD_to_COMMAND of ct_EVAL_CMD
-  | CT_coerce_IMPEXP_to_COMMAND of ct_IMPEXP
   | CT_coerce_SECTION_BEGIN_to_COMMAND of ct_SECTION_BEGIN
   | CT_coerce_THEOREM_GOAL_to_COMMAND of ct_THEOREM_GOAL
   | CT_abort of ct_ID_OPT_OR_ALL
   | CT_abstraction of ct_ID * ct_FORMULA * ct_INT_LIST
   | CT_add_natural_feature of ct_NATURAL_FEATURE * ct_ID
   | CT_addpath of ct_STRING * ct_ID_OPT
+  | CT_arguments_scope of ct_ID * ct_ID_OPT_LIST
+  | CT_bind_scope of ct_ID * ct_ID_NE_LIST
   | CT_cd of ct_STRING_OPT
   | CT_check of ct_FORMULA
   | CT_class of ct_ID
+  | CT_close_scope of ct_ID
   | CT_coercion of ct_LOCAL_OPT * ct_IDENTITY_OPT * ct_ID * ct_ID * ct_ID
   | CT_cofix_decl of ct_COFIX_REC_LIST
   | CT_compile_module of ct_VERBOSE_OPT * ct_ID * ct_STRING_OPT
+  | CT_define_notation of ct_STRING * ct_FORMULA * ct_MODIFIER_LIST * ct_ID_OPT
   | CT_definition of ct_DEFN * ct_ID * ct_BINDER_LIST * ct_DEF_BODY * ct_FORMULA_OPT
+  | CT_delim_scope of ct_ID * ct_ID
   | CT_delpath of ct_STRING
   | CT_derive_depinversion of ct_INV_TYPE * ct_ID * ct_FORMULA * ct_SORT_TYPE
   | CT_derive_inversion of ct_INV_TYPE * ct_INT_OPT * ct_ID * ct_ID
   | CT_derive_inversion_with of ct_INV_TYPE * ct_ID * ct_FORMULA * ct_SORT_TYPE
   | CT_explain_proof of ct_INT_LIST
   | CT_explain_prooftree of ct_INT_LIST
+  | CT_export_id of ct_ID_NE_LIST
   | CT_fix_decl of ct_FIX_REC_LIST
   | CT_focus of ct_INT_OPT
   | CT_go of ct_INT_OR_LOCN
@@ -73,18 +74,24 @@ and ct_COMMAND =
   | CT_hint_extern of ct_INT * ct_FORMULA * ct_TACTIC_COM * ct_ID_LIST
   | CT_hintrewrite of ct_ORIENTATION * ct_FORMULA_NE_LIST * ct_ID * ct_TACTIC_COM
   | CT_hints of ct_ID * ct_ID_NE_LIST * ct_ID_LIST
-  | CT_implicits of ct_ID * ct_INT_LIST
+  | CT_implicits of ct_ID * ct_ID_LIST
+  | CT_import_id of ct_ID_NE_LIST
   | CT_ind_scheme of ct_SCHEME_SPEC_LIST
-  | CT_infix of ct_ASSOC * ct_INT * ct_STRING * ct_ID
+  | CT_infix of ct_STRING * ct_ID * ct_MODIFIER_LIST * ct_ID_OPT
   | CT_inspect of ct_INT
   | CT_kill_node of ct_INT
   | CT_load of ct_VERBOSE_OPT * ct_ID_OR_STRING
+  | CT_local_close_scope of ct_ID
+  | CT_local_define_notation of ct_STRING * ct_FORMULA * ct_MODIFIER_LIST * ct_ID_OPT
   | CT_local_hint_destruct of ct_ID * ct_INT * ct_DESTRUCT_LOCATION * ct_FORMULA * ct_TACTIC_COM * ct_ID_LIST
   | CT_local_hint_extern of ct_INT * ct_FORMULA * ct_TACTIC_COM * ct_ID_LIST
   | CT_local_hints of ct_ID * ct_ID_NE_LIST * ct_ID_LIST
+  | CT_local_infix of ct_STRING * ct_ID * ct_MODIFIER_LIST * ct_ID_OPT
+  | CT_local_open_scope of ct_ID
   | CT_locate of ct_ID
   | CT_locate_file of ct_STRING
   | CT_locate_lib of ct_ID
+  | CT_locate_notation of ct_STRING
   | CT_mind_decl of ct_CO_IND * ct_IND_SPEC_LIST
   | CT_ml_add_path of ct_STRING
   | CT_ml_declare_modules of ct_STRING_NE_LIST
@@ -93,24 +100,34 @@ and ct_COMMAND =
   | CT_module of ct_ID
   | CT_omega_flag of ct_OMEGA_MODE * ct_OMEGA_FEATURE
   | CT_opaque of ct_ID_NE_LIST
-  | CT_parameter of ct_BINDER
+  | CT_open_scope of ct_ID
+  | CT_print
+  | CT_print_about of ct_ID
   | CT_print_all
   | CT_print_classes
   | CT_print_coercions
   | CT_print_grammar of ct_GRAMMAR
   | CT_print_graph
   | CT_print_hint of ct_ID_OPT
-  | CT_print_hintdb of ct_ID
+  | CT_print_hintdb of ct_ID_OR_STAR
   | CT_print_id of ct_ID
+  | CT_print_implicit of ct_ID
   | CT_print_loadpath
+  | CT_print_module of ct_ID
+  | CT_print_module_type of ct_ID
   | CT_print_modules
   | CT_print_natural of ct_ID
   | CT_print_natural_feature of ct_NATURAL_FEATURE
   | CT_print_opaqueid of ct_ID
   | CT_print_path of ct_ID * ct_ID
   | CT_print_proof of ct_ID
+  | CT_print_scope of ct_ID
+  | CT_print_scopes
   | CT_print_section of ct_ID
   | CT_print_states
+  | CT_print_tables
+  | CT_print_universes of ct_STRING_OPT
+  | CT_print_visibility of ct_ID_OPT
   | CT_proof of ct_FORMULA
   | CT_proof_no_op
   | CT_pwd
@@ -121,7 +138,8 @@ and ct_COMMAND =
   | CT_recaddpath of ct_STRING * ct_ID_OPT
   | CT_record of ct_COERCION_OPT * ct_ID * ct_BINDER_LIST * ct_FORMULA * ct_ID_OPT * ct_RECCONSTR_LIST
   | CT_remove_natural_feature of ct_NATURAL_FEATURE * ct_ID
-  | CT_require of ct_IMPEXP * ct_SPEC_OPT * ct_ID * ct_STRING_OPT
+  | CT_require of ct_IMPEXP * ct_SPEC_OPT * ct_ID_NE_LIST_OR_STRING
+  | CT_reserve of ct_ID_NE_LIST * ct_FORMULA
   | CT_reset of ct_ID
   | CT_reset_section of ct_ID
   | CT_restart
@@ -130,6 +148,7 @@ and ct_COMMAND =
   | CT_save of ct_THM_OPT * ct_ID_OPT
   | CT_scomments of ct_SCOMMENT_CONTENT_LIST
   | CT_search of ct_ID * ct_IN_OR_OUT_MODULES
+  | CT_search_about of ct_ID_OR_STRING_NE_LIST * ct_IN_OR_OUT_MODULES
   | CT_search_pattern of ct_FORMULA * ct_IN_OR_OUT_MODULES
   | CT_search_rewrite of ct_FORMULA * ct_IN_OR_OUT_MODULES
   | CT_section_end of ct_ID
@@ -138,8 +157,11 @@ and ct_COMMAND =
   | CT_set_natural_default
   | CT_sethyp of ct_INT
   | CT_setundo of ct_INT
+  | CT_show_existentials
   | CT_show_goal of ct_INT_OPT
-  | CT_show_implicits
+  | CT_show_implicit of ct_INT
+  | CT_show_intro
+  | CT_show_intros
   | CT_show_node
   | CT_show_proof
   | CT_show_proofs
@@ -151,7 +173,7 @@ and ct_COMMAND =
   | CT_tactic_definition of ct_ID * ct_ID_UNIT_LIST * ct_TACTIC_COM
   | CT_test_natural_feature of ct_NATURAL_FEATURE * ct_ID
   | CT_theorem_struct of ct_THEOREM_GOAL * ct_PROOF_SCRIPT
-  | CT_token of ct_STRING
+  | CT_time of ct_COMMAND
   | CT_transparent of ct_ID_NE_LIST
   | CT_undo of ct_INT_OPT
   | CT_unfocus
@@ -296,9 +318,14 @@ and ct_ID_NE_LIST =
 and ct_ID_NE_LIST_OR_STAR =
     CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR of ct_ID_NE_LIST
   | CT_coerce_STAR_to_ID_NE_LIST_OR_STAR of ct_STAR
+and ct_ID_NE_LIST_OR_STRING =
+    CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STRING of ct_ID_NE_LIST
+  | CT_coerce_STRING_to_ID_NE_LIST_OR_STRING of ct_STRING
 and ct_ID_OPT =
     CT_coerce_ID_to_ID_OPT of ct_ID
   | CT_coerce_NONE_to_ID_OPT of ct_NONE
+and ct_ID_OPT_LIST =
+    CT_id_opt_list of ct_ID_OPT list
 and ct_ID_OPT_NE_LIST =
     CT_id_opt_ne_list of ct_ID_OPT * ct_ID_OPT list
 and ct_ID_OPT_OR_ALL =
@@ -311,9 +338,14 @@ and ct_ID_OR_INT_OPT =
     CT_coerce_ID_OPT_to_ID_OR_INT_OPT of ct_ID_OPT
   | CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT of ct_ID_OR_INT
   | CT_coerce_INT_OPT_to_ID_OR_INT_OPT of ct_INT_OPT
+and ct_ID_OR_STAR =
+    CT_coerce_ID_to_ID_OR_STAR of ct_ID
+  | CT_coerce_STAR_to_ID_OR_STAR of ct_STAR
 and ct_ID_OR_STRING =
     CT_coerce_ID_to_ID_OR_STRING of ct_ID
   | CT_coerce_STRING_to_ID_OR_STRING of ct_STRING
+and ct_ID_OR_STRING_NE_LIST =
+    CT_id_or_string_ne_list of ct_ID_OR_STRING * ct_ID_OR_STRING list
 and ct_ID_UNIT =
     CT_coerce_ID_to_ID_UNIT of ct_ID
   | CT_unit
@@ -322,7 +354,8 @@ and ct_ID_UNIT_LIST =
 and ct_ID_UNIT_NE_LIST =
     CT_id_unit_ne_list of ct_ID_UNIT * ct_ID_UNIT list
 and ct_IMPEXP =
-    CT_export
+    CT_coerce_NONE_to_IMPEXP of ct_NONE
+  | CT_export
   | CT_import
 and ct_IND_SPEC =
     CT_ind_spec of ct_ID * ct_BINDER_LIST * ct_FORMULA * ct_CONSTR_LIST * ct_DECL_NOTATION_OPT
@@ -346,6 +379,9 @@ and ct_INT_OPT =
 and ct_INT_OR_LOCN =
     CT_coerce_INT_to_INT_OR_LOCN of ct_INT
   | CT_coerce_LOCN_to_INT_OR_LOCN of ct_LOCN
+and ct_INT_OR_NEXT =
+    CT_coerce_INT_to_INT_OR_NEXT of ct_INT
+  | CT_next_level
 and ct_INV_TYPE =
     CT_inv_clear
   | CT_inv_regular
@@ -388,6 +424,17 @@ and ct_MATCH_TAC_RULE =
     CT_match_tac_rule of ct_CONTEXT_PATTERN * ct_LET_VALUE
 and ct_MATCH_TAC_RULES =
     CT_match_tac_rules of ct_MATCH_TAC_RULE * ct_MATCH_TAC_RULE list
+and ct_MODIFIER =
+    CT_entry_type of ct_ID * ct_ID
+  | CT_format of ct_STRING
+  | CT_lefta
+  | CT_nona
+  | CT_only_parsing
+  | CT_righta
+  | CT_set_item_level of ct_ID_NE_LIST * ct_INT_OR_NEXT
+  | CT_set_level of ct_INT
+and ct_MODIFIER_LIST =
+    CT_modifier_list of ct_MODIFIER list
 and ct_NATURAL_FEATURE =
     CT_contractible
   | CT_implicit
@@ -631,7 +678,7 @@ and ct_TEXT =
   | CT_text_v of ct_TEXT list
 and ct_THEOREM_GOAL =
     CT_goal of ct_FORMULA
-  | CT_theorem_goal of ct_DEFN_OR_THM * ct_ID * ct_FORMULA
+  | CT_theorem_goal of ct_DEFN_OR_THM * ct_ID * ct_BINDER_LIST * ct_FORMULA
 and ct_THM =
     CT_thm of string
 and ct_THM_OPT =
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 81df96b67..f39e21046 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -14,12 +14,7 @@ let fATOM s1 =
 
 let f_atom_string = print_string;;
 let f_atom_int = print_int;;
-let rec fASSOC = function
-| CT_coerce_NONE_to_ASSOC x -> fNONE x
-| CT_lefta -> fNODE "lefta" 0
-| CT_nona -> fNODE "nona" 0
-| CT_righta -> fNODE "righta" 0
-and fAST = function
+let rec fAST = function
 | CT_coerce_ID_OR_INT_to_AST x -> fID_OR_INT x
 | CT_coerce_ID_OR_STRING_to_AST x -> fID_OR_STRING x
 | CT_astnode(x1, x2) ->
@@ -46,6 +41,10 @@ and fBINARY = function
    fID_OPT_NE_LIST x1;
    fFORMULA x2;
    fNODE "binder" 2
+| CT_binder_coercion(x1, x2) ->
+   fID_OPT_NE_LIST x1;
+   fFORMULA x2;
+   fNODE "binder_coercion" 2
 and fBINDER_LIST = function
 | CT_binder_list l ->
    (List.iter fBINDER l);
@@ -101,7 +100,6 @@ and fCOFIX_TAC_LIST = function
 and fCOMMAND = function
 | CT_coerce_COMMAND_LIST_to_COMMAND x -> fCOMMAND_LIST x
 | CT_coerce_EVAL_CMD_to_COMMAND x -> fEVAL_CMD x
-| CT_coerce_IMPEXP_to_COMMAND x -> fIMPEXP x
 | CT_coerce_SECTION_BEGIN_to_COMMAND x -> fSECTION_BEGIN x
 | CT_coerce_THEOREM_GOAL_to_COMMAND x -> fTHEOREM_GOAL x
 | CT_abort(x1) ->
@@ -120,6 +118,14 @@ and fCOMMAND = function
    fSTRING x1;
    fID_OPT x2;
    fNODE "addpath" 2
+| CT_arguments_scope(x1, x2) ->
+   fID x1;
+   fID_OPT_LIST x2;
+   fNODE "arguments_scope" 2
+| CT_bind_scope(x1, x2) ->
+   fID x1;
+   fID_NE_LIST x2;
+   fNODE "bind_scope" 2
 | CT_cd(x1) ->
    fSTRING_OPT x1;
    fNODE "cd" 1
@@ -129,6 +135,9 @@ and fCOMMAND = function
 | CT_class(x1) ->
    fID x1;
    fNODE "class" 1
+| CT_close_scope(x1) ->
+   fID x1;
+   fNODE "close_scope" 1
 | CT_coercion(x1, x2, x3, x4, x5) ->
    fLOCAL_OPT x1;
    fIDENTITY_OPT x2;
@@ -144,6 +153,12 @@ and fCOMMAND = function
    fID x2;
    fSTRING_OPT x3;
    fNODE "compile_module" 3
+| CT_define_notation(x1, x2, x3, x4) ->
+   fSTRING x1;
+   fFORMULA x2;
+   fMODIFIER_LIST x3;
+   fID_OPT x4;
+   fNODE "define_notation" 4
 | CT_definition(x1, x2, x3, x4, x5) ->
    fDEFN x1;
    fID x2;
@@ -151,6 +166,10 @@ and fCOMMAND = function
    fDEF_BODY x4;
    fFORMULA_OPT x5;
    fNODE "definition" 5
+| CT_delim_scope(x1, x2) ->
+   fID x1;
+   fID x2;
+   fNODE "delim_scope" 2
 | CT_delpath(x1) ->
    fSTRING x1;
    fNODE "delpath" 1
@@ -178,6 +197,9 @@ and fCOMMAND = function
 | CT_explain_prooftree(x1) ->
    fINT_LIST x1;
    fNODE "explain_prooftree" 1
+| CT_export_id(x1) ->
+   fID_NE_LIST x1;
+   fNODE "export_id" 1
 | CT_fix_decl(x1) ->
    fFIX_REC_LIST x1;
    fNODE "fix_decl" 1
@@ -215,16 +237,19 @@ and fCOMMAND = function
    fNODE "hints" 3
 | CT_implicits(x1, x2) ->
    fID x1;
-   fINT_LIST x2;
+   fID_LIST x2;
    fNODE "implicits" 2
+| CT_import_id(x1) ->
+   fID_NE_LIST x1;
+   fNODE "import_id" 1
 | CT_ind_scheme(x1) ->
    fSCHEME_SPEC_LIST x1;
    fNODE "ind_scheme" 1
 | CT_infix(x1, x2, x3, x4) ->
-   fASSOC x1;
-   fINT x2;
-   fSTRING x3;
-   fID x4;
+   fSTRING x1;
+   fID x2;
+   fMODIFIER_LIST x3;
+   fID_OPT x4;
    fNODE "infix" 4
 | CT_inspect(x1) ->
    fINT x1;
@@ -236,6 +261,15 @@ and fCOMMAND = function
    fVERBOSE_OPT x1;
    fID_OR_STRING x2;
    fNODE "load" 2
+| CT_local_close_scope(x1) ->
+   fID x1;
+   fNODE "local_close_scope" 1
+| CT_local_define_notation(x1, x2, x3, x4) ->
+   fSTRING x1;
+   fFORMULA x2;
+   fMODIFIER_LIST x3;
+   fID_OPT x4;
+   fNODE "local_define_notation" 4
 | CT_local_hint_destruct(x1, x2, x3, x4, x5, x6) ->
    fID x1;
    fINT x2;
@@ -255,6 +289,15 @@ and fCOMMAND = function
    fID_NE_LIST x2;
    fID_LIST x3;
    fNODE "local_hints" 3
+| CT_local_infix(x1, x2, x3, x4) ->
+   fSTRING x1;
+   fID x2;
+   fMODIFIER_LIST x3;
+   fID_OPT x4;
+   fNODE "local_infix" 4
+| CT_local_open_scope(x1) ->
+   fID x1;
+   fNODE "local_open_scope" 1
 | CT_locate(x1) ->
    fID x1;
    fNODE "locate" 1
@@ -264,6 +307,9 @@ and fCOMMAND = function
 | CT_locate_lib(x1) ->
    fID x1;
    fNODE "locate_lib" 1
+| CT_locate_notation(x1) ->
+   fSTRING x1;
+   fNODE "locate_notation" 1
 | CT_mind_decl(x1, x2) ->
    fCO_IND x1;
    fIND_SPEC_LIST x2;
@@ -286,9 +332,13 @@ and fCOMMAND = function
 | CT_opaque(x1) ->
    fID_NE_LIST x1;
    fNODE "opaque" 1
-| CT_parameter(x1) ->
-   fBINDER x1;
-   fNODE "parameter" 1
+| CT_open_scope(x1) ->
+   fID x1;
+   fNODE "open_scope" 1
+| CT_print -> fNODE "print" 0
+| CT_print_about(x1) ->
+   fID x1;
+   fNODE "print_about" 1
 | CT_print_all -> fNODE "print_all" 0
 | CT_print_classes -> fNODE "print_classes" 0
 | CT_print_coercions -> fNODE "print_coercions" 0
@@ -300,12 +350,21 @@ and fCOMMAND = function
    fID_OPT x1;
    fNODE "print_hint" 1
 | CT_print_hintdb(x1) ->
-   fID x1;
+   fID_OR_STAR x1;
    fNODE "print_hintdb" 1
 | CT_print_id(x1) ->
    fID x1;
    fNODE "print_id" 1
+| CT_print_implicit(x1) ->
+   fID x1;
+   fNODE "print_implicit" 1
 | CT_print_loadpath -> fNODE "print_loadpath" 0
+| CT_print_module(x1) ->
+   fID x1;
+   fNODE "print_module" 1
+| CT_print_module_type(x1) ->
+   fID x1;
+   fNODE "print_module_type" 1
 | CT_print_modules -> fNODE "print_modules" 0
 | CT_print_natural(x1) ->
    fID x1;
@@ -323,10 +382,21 @@ and fCOMMAND = function
 | CT_print_proof(x1) ->
    fID x1;
    fNODE "print_proof" 1
+| CT_print_scope(x1) ->
+   fID x1;
+   fNODE "print_scope" 1
+| CT_print_scopes -> fNODE "print_scopes" 0
 | CT_print_section(x1) ->
    fID x1;
    fNODE "print_section" 1
 | CT_print_states -> fNODE "print_states" 0
+| CT_print_tables -> fNODE "print_tables" 0
+| CT_print_universes(x1) ->
+   fSTRING_OPT x1;
+   fNODE "print_universes" 1
+| CT_print_visibility(x1) ->
+   fID_OPT x1;
+   fNODE "print_visibility" 1
 | CT_proof(x1) ->
    fFORMULA x1;
    fNODE "proof" 1
@@ -358,12 +428,15 @@ and fCOMMAND = function
    fNATURAL_FEATURE x1;
    fID x2;
    fNODE "remove_natural_feature" 2
-| CT_require(x1, x2, x3, x4) ->
+| CT_require(x1, x2, x3) ->
    fIMPEXP x1;
    fSPEC_OPT x2;
-   fID x3;
-   fSTRING_OPT x4;
-   fNODE "require" 4
+   fID_NE_LIST_OR_STRING x3;
+   fNODE "require" 3
+| CT_reserve(x1, x2) ->
+   fID_NE_LIST x1;
+   fFORMULA x2;
+   fNODE "reserve" 2
 | CT_reset(x1) ->
    fID x1;
    fNODE "reset" 1
@@ -388,6 +461,10 @@ and fCOMMAND = function
    fID x1;
    fIN_OR_OUT_MODULES x2;
    fNODE "search" 2
+| CT_search_about(x1, x2) ->
+   fID_OR_STRING_NE_LIST x1;
+   fIN_OR_OUT_MODULES x2;
+   fNODE "search_about" 2
 | CT_search_pattern(x1, x2) ->
    fFORMULA x1;
    fIN_OR_OUT_MODULES x2;
@@ -414,10 +491,15 @@ and fCOMMAND = function
 | CT_setundo(x1) ->
    fINT x1;
    fNODE "setundo" 1
+| CT_show_existentials -> fNODE "show_existentials" 0
 | CT_show_goal(x1) ->
    fINT_OPT x1;
    fNODE "show_goal" 1
-| CT_show_implicits -> fNODE "show_implicits" 0
+| CT_show_implicit(x1) ->
+   fINT x1;
+   fNODE "show_implicit" 1
+| CT_show_intro -> fNODE "show_intro" 0
+| CT_show_intros -> fNODE "show_intros" 0
 | CT_show_node -> fNODE "show_node" 0
 | CT_show_proof -> fNODE "show_proof" 0
 | CT_show_proofs -> fNODE "show_proofs" 0
@@ -446,9 +528,9 @@ and fCOMMAND = function
    fTHEOREM_GOAL x1;
    fPROOF_SCRIPT x2;
    fNODE "theorem_struct" 2
-| CT_token(x1) ->
-   fSTRING x1;
-   fNODE "token" 1
+| CT_time(x1) ->
+   fCOMMAND x1;
+   fNODE "time" 1
 | CT_transparent(x1) ->
    fID_NE_LIST x1;
    fNODE "transparent" 1
@@ -766,9 +848,16 @@ and fID_NE_LIST = function
 and fID_NE_LIST_OR_STAR = function
 | CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR x -> fID_NE_LIST x
 | CT_coerce_STAR_to_ID_NE_LIST_OR_STAR x -> fSTAR x
+and fID_NE_LIST_OR_STRING = function
+| CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STRING x -> fID_NE_LIST x
+| CT_coerce_STRING_to_ID_NE_LIST_OR_STRING x -> fSTRING x
 and fID_OPT = function
 | CT_coerce_ID_to_ID_OPT x -> fID x
 | CT_coerce_NONE_to_ID_OPT x -> fNONE x
+and fID_OPT_LIST = function
+| CT_id_opt_list l ->
+   (List.iter fID_OPT l);
+   fNODE "id_opt_list" (List.length l)
 and fID_OPT_NE_LIST = function
 | CT_id_opt_ne_list(x,l) ->
    fID_OPT x;
@@ -784,9 +873,17 @@ and fID_OR_INT_OPT = function
 | CT_coerce_ID_OPT_to_ID_OR_INT_OPT x -> fID_OPT x
 | CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT x -> fID_OR_INT x
 | CT_coerce_INT_OPT_to_ID_OR_INT_OPT x -> fINT_OPT x
+and fID_OR_STAR = function
+| CT_coerce_ID_to_ID_OR_STAR x -> fID x
+| CT_coerce_STAR_to_ID_OR_STAR x -> fSTAR x
 and fID_OR_STRING = function
 | CT_coerce_ID_to_ID_OR_STRING x -> fID x
 | CT_coerce_STRING_to_ID_OR_STRING x -> fSTRING x
+and fID_OR_STRING_NE_LIST = function
+| CT_id_or_string_ne_list(x,l) ->
+   fID_OR_STRING x;
+   (List.iter fID_OR_STRING l);
+   fNODE "id_or_string_ne_list" (1 + (List.length l))
 and fID_UNIT = function
 | CT_coerce_ID_to_ID_UNIT x -> fID x
 | CT_unit -> fNODE "unit" 0
@@ -800,6 +897,7 @@ and fID_UNIT_NE_LIST = function
    (List.iter fID_UNIT l);
    fNODE "id_unit_ne_list" (1 + (List.length l))
 and fIMPEXP = function
+| CT_coerce_NONE_to_IMPEXP x -> fNONE x
 | CT_export -> fNODE "export" 0
 | CT_import -> fNODE "import" 0
 and fIND_SPEC = function
@@ -844,6 +942,9 @@ and fINT_OPT = function
 and fINT_OR_LOCN = function
 | CT_coerce_INT_to_INT_OR_LOCN x -> fINT x
 | CT_coerce_LOCN_to_INT_OR_LOCN x -> fLOCN x
+and fINT_OR_NEXT = function
+| CT_coerce_INT_to_INT_OR_NEXT x -> fINT x
+| CT_next_level -> fNODE "next_level" 0
 and fINV_TYPE = function
 | CT_inv_clear -> fNODE "inv_clear" 0
 | CT_inv_regular -> fNODE "inv_regular" 0
@@ -934,6 +1035,29 @@ and fMATCH_TAC_RULES = function
    fMATCH_TAC_RULE x;
    (List.iter fMATCH_TAC_RULE l);
    fNODE "match_tac_rules" (1 + (List.length l))
+and fMODIFIER = function
+| CT_entry_type(x1, x2) ->
+   fID x1;
+   fID x2;
+   fNODE "entry_type" 2
+| CT_format(x1) ->
+   fSTRING x1;
+   fNODE "format" 1
+| CT_lefta -> fNODE "lefta" 0
+| CT_nona -> fNODE "nona" 0
+| CT_only_parsing -> fNODE "only_parsing" 0
+| CT_righta -> fNODE "righta" 0
+| CT_set_item_level(x1, x2) ->
+   fID_NE_LIST x1;
+   fINT_OR_NEXT x2;
+   fNODE "set_item_level" 2
+| CT_set_level(x1) ->
+   fINT x1;
+   fNODE "set_level" 1
+and fMODIFIER_LIST = function
+| CT_modifier_list l ->
+   (List.iter fMODIFIER l);
+   fNODE "modifier_list" (List.length l)
 and fNATURAL_FEATURE = function
 | CT_contractible -> fNODE "contractible" 0
 | CT_implicit -> fNODE "implicit" 0
@@ -1560,11 +1684,12 @@ and fTHEOREM_GOAL = function
 | CT_goal(x1) ->
    fFORMULA x1;
    fNODE "goal" 1
-| CT_theorem_goal(x1, x2, x3) ->
+| CT_theorem_goal(x1, x2, x3, x4) ->
    fDEFN_OR_THM x1;
    fID x2;
-   fFORMULA x3;
-   fNODE "theorem_goal" 3
+   fBINDER_LIST x3;
+   fFORMULA x4;
+   fNODE "theorem_goal" 4
 and fTHM = function
 | CT_thm x -> fATOM "thm";
    (f_atom_string x);
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 0ca53aa17..dd7aa015f 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1291,8 +1291,14 @@ let xlate_thm x = CT_thm (match x with
 
 
 let xlate_defn x = CT_defn (match x with
- | Local -> "Local"
- | Global -> "Definition")
+ | (Local, Definition) -> "Local"
+ | (Global, Definition) -> "Definition"
+ | (Global, Coercion) -> "SubClass"
+ | (Local, Coercion) -> "Local SubClass"
+ | (Global,CanonicalStructure) -> "Canonical Structure"
+ | (Local, CanonicalStructure) -> 
+     xlate_error "Local CanonicalStructure not parsed"
+ | (_, SubClass) -> xlate_error "Obsolete SubClass not supported")
 
 let xlate_var x = CT_var (match x with
  | (Global,Definitional) -> "Parameter"
@@ -1355,8 +1361,9 @@ let build_record_field_list l =
 let get_require_flags impexp spec =
  let ct_impexp =
   match impexp with
-  | false -> CT_import
-  | true -> CT_export in
+  | None -> CT_coerce_NONE_to_IMPEXP CT_none
+  | Some false -> CT_import
+  | Some true -> CT_export in
  let ct_spec =
   match spec with
   | None -> ctv_SPEC_OPT_NONE
@@ -1374,13 +1381,17 @@ let cvt_optional_eval_for_definition c1 optional_eval =
 	      xlate_formula c1))
 
 let cvt_vernac_binder = function
-  | (id::idl,c) ->
-     CT_binder(
-       CT_id_opt_ne_list 
-         (xlate_ident_opt (Some (snd id)),
-          List.map (fun id -> xlate_ident_opt (Some (snd id))) idl),
-         xlate_formula c)
-  | ([],_) -> xlate_error "Empty list of vernac binder"
+  | b,(id::idl,c) ->
+      let l,t = 
+	CT_id_opt_ne_list 
+          (xlate_ident_opt (Some (snd id)),
+           List.map (fun id -> xlate_ident_opt (Some (snd id))) idl),
+          xlate_formula c in
+	if b then
+	  CT_binder(l,t)
+	else
+	  CT_binder_coercion(l,t)
+  | _, _ -> xlate_error "binder with no left part, rejected";;
 
 let cvt_vernac_binders = function
     a::args -> CT_binder_ne_list(cvt_vernac_binder a, List.map cvt_vernac_binder args)
@@ -1404,7 +1415,32 @@ let translate_opt_notation_decl = function
 	   | Some id -> CT_coerce_ID_to_ID_OPT (CT_ident id) in
        CT_decl_notation(CT_string s, xlate_formula f, tr_sc);;
 
-let xlate_vernac =
+let xlate_level = function
+    Extend.NumLevel n -> CT_coerce_INT_to_INT_OR_NEXT(CT_int n)
+  | Extend.NextLevel -> CT_next_level;;
+
+let xlate_syntax_modifier = function
+    Extend.SetItemLevel((s::sl), level) ->
+      CT_set_item_level
+	(CT_id_ne_list(CT_ident s, List.map (fun s -> CT_ident s) sl),
+	 xlate_level level)
+  | Extend.SetItemLevel([], _) -> assert false
+  | Extend.SetLevel level -> CT_set_level (CT_int level)
+  | Extend.SetAssoc Gramext.LeftA -> CT_lefta
+  | Extend.SetAssoc Gramext.RightA -> CT_righta
+  | Extend.SetAssoc Gramext.NonA -> CT_nona
+  | Extend.SetEntryType(x,typ) ->
+      CT_entry_type(CT_ident x,
+		 match typ with
+		     Extend.ETIdent -> CT_ident "ident"
+		   | Extend.ETReference -> CT_ident "global"
+		   | Extend.ETBigint -> CT_ident "bigint"
+		   | _ -> xlate_error "syntax_type not parsed")
+  | Extend.SetOnlyParsing -> CT_only_parsing
+  | Extend.SetFormat(_,s) -> CT_format(CT_string s);;
+
+
+let rec xlate_vernac =
  function
    | VernacDeclareTacticDefinition (false,[(_,id),TacFun (largs,tac)]) ->
        let fst, rest = xlate_largs_to_id_unit largs in
@@ -1480,7 +1516,6 @@ let xlate_vernac =
 	| _ -> assert false in
       CT_hintrewrite(ct_orient, f_ne_list, CT_ident base, xlate_tactic t)
   | VernacHints (local,dbnames,h) ->
-      (* TODO: locality flag *)
       let dblist = CT_id_list(List.map (fun x -> CT_ident x) dbnames) in
       (match h with
 	| HintsConstructors (None, l) ->
@@ -1562,7 +1597,8 @@ let xlate_vernac =
   | VernacEndProof (Proved (b,Some ((_,s),None))) ->
       CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"),
        ctf_ID_OPT_SOME (xlate_ident s))
-  | VernacEndProof Admitted -> xlate_error "TODO: Admitted"
+  | VernacEndProof Admitted ->
+      CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Admitted"), ctv_ID_OPT_NONE)
   | VernacSetOpacity (false, id :: idl) ->
             CT_transparent(CT_id_ne_list(loc_qualid_to_ct_ID id,
                    List.map loc_qualid_to_ct_ID idl))
@@ -1576,8 +1612,12 @@ let xlate_vernac =
   | VernacShow ShowProof -> CT_show_proof
   | VernacShow ShowTree -> CT_show_tree
   | VernacShow ShowProofNames -> CT_show_proofs
-  | VernacShow (ShowIntros _|ShowGoalImplicitly _|ShowExistentials|ShowScript)
-      -> xlate_error "TODO: Show Intro/Intros/Implicits/Existentials/Script"
+  | VernacShow (ShowIntros true) -> CT_show_intros
+  | VernacShow (ShowIntros false) -> CT_show_intro
+  | VernacShow (ShowGoalImplicitly None) -> CT_show_implicit (CT_int 1)
+  | VernacShow (ShowGoalImplicitly (Some n)) -> CT_show_implicit (CT_int n)
+  | VernacShow ShowExistentials -> CT_show_existentials
+  | VernacShow ShowScript -> CT_show_script
   | VernacGo arg -> CT_go (xlate_locn arg)
   | VernacShow ExplainProof l -> CT_explain_proof (nums_to_int_list l)
   | VernacShow ExplainTree l ->
@@ -1591,10 +1631,12 @@ let xlate_vernac =
 	| PrintSectionContext id -> CT_print_section (loc_qualid_to_ct_ID id)
 	| PrintModules -> CT_print_modules
 	| PrintGrammar (phylum, name) -> CT_print_grammar CT_grammar_none
-	| PrintHintDb -> CT_print_hint (CT_coerce_NONE_to_ID_OPT CT_none)
-	| PrintHintDbName id -> CT_print_hintdb (CT_ident id)
+	| PrintHintDb -> CT_print_hintdb (CT_coerce_STAR_to_ID_OR_STAR CT_star)
+	| PrintHintDbName id -> 
+	    CT_print_hintdb (CT_coerce_ID_to_ID_OR_STAR (CT_ident id))
 	| PrintHint id ->
 	    CT_print_hint (CT_coerce_ID_to_ID_OPT (loc_qualid_to_ct_ID id))
+	| PrintHintGoal -> CT_print_hint ctv_ID_OPT_NONE
 	| PrintLoadPath -> CT_print_loadpath
 	| PrintMLLoadPath -> CT_ml_print_path
 	| PrintMLModules -> CT_ml_print_modules
@@ -1604,49 +1646,66 @@ let xlate_vernac =
 	| PrintCoercionPaths (id1, id2) -> 
 	    CT_print_path (xlate_class id1, xlate_class id2)
 	| PrintInspect n -> CT_inspect (CT_int n)
-	| PrintUniverses _ -> xlate_error "TODO: Dump Universes"
-	| PrintHintGoal -> xlate_error "TODO: Print Hint"
-	| PrintLocalContext -> xlate_error "TODO: Print"
-	| PrintTables -> xlate_error "TODO: Print Tables"
-        | PrintModuleType _ -> xlate_error "TODO: Print Module Type"
-        | PrintModule _ -> xlate_error "TODO: Print Module"
-        | PrintScopes -> xlate_error "TODO: Print Scopes"
-        | PrintScope _ -> xlate_error "TODO: Print Scope"
-	| PrintVisibility _ -> xlate_error "TODO: Print Visibility"
-        | PrintAbout _ -> xlate_error "TODO: Print About"
-	| _ -> xlate_error "TODO: Print")
+        | PrintUniverses None -> CT_print_universes ctf_STRING_OPT_NONE
+	| PrintUniverses (Some s) ->
+	    CT_print_universes (ctf_STRING_OPT_SOME (CT_string s))
+	| PrintLocalContext -> CT_print
+	| PrintTables -> CT_print_tables
+        | PrintModuleType a -> CT_print_module_type (loc_qualid_to_ct_ID a)
+        | PrintModule a -> CT_print_module (loc_qualid_to_ct_ID a)
+        | PrintScopes -> CT_print_scopes
+        | PrintScope id -> CT_print_scope (CT_ident id)
+	| PrintVisibility id_opt ->
+	    CT_print_visibility 
+	      (match id_opt with
+		   Some id -> CT_coerce_ID_to_ID_OPT(CT_ident id)
+		 | None -> ctv_ID_OPT_NONE)
+        | PrintAbout qid -> CT_print_about(loc_qualid_to_ct_ID qid)
+	| PrintImplicit qid -> CT_print_implicit(loc_qualid_to_ct_ID qid))
   | VernacBeginSection (_,id) ->
       CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
   | VernacEndSegment (_,id) -> CT_section_end (xlate_ident id)
-  | VernacStartTheoremProof (k, (_,s), ([],c), _, _) ->
+  | VernacStartTheoremProof (k, (_,s), (bl,c), _, _) ->
       CT_coerce_THEOREM_GOAL_to_COMMAND(
-	CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s,xlate_formula c))
-  | VernacStartTheoremProof (k, s, (bl,c), _, _) -> 
-      xlate_error "TODO: VernacStartTheoremProof"
+	CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s,
+           xlate_binder_list bl, xlate_formula c))
   | VernacSuspend -> CT_suspend
   | VernacResume idopt -> CT_resume (xlate_ident_opt (option_app snd idopt))
-  | VernacDefinition ((k,_),(_,s),ProveBody (bl,typ),_) ->
-      if bl <> [] then xlate_error "TODO: Def bindings";
-      CT_coerce_THEOREM_GOAL_to_COMMAND(
-	CT_theorem_goal (CT_coerce_DEFN_to_DEFN_OR_THM (xlate_defn k), xlate_ident s,xlate_formula typ))
-  | VernacDefinition ((kind,_),(_,s),DefineBody(bl,red_option,c,typ_opt),_) ->
+  | VernacDefinition (k,(_,s),ProveBody (bl,typ),_) ->
+      CT_coerce_THEOREM_GOAL_to_COMMAND
+	(CT_theorem_goal
+	   (CT_coerce_DEFN_to_DEFN_OR_THM (xlate_defn k),
+	    xlate_ident s, xlate_binder_list bl, xlate_formula typ))
+  | VernacDefinition (kind,(_,s),DefineBody(bl,red_option,c,typ_opt),_) ->
       CT_definition
 	(xlate_defn kind, xlate_ident s, xlate_binder_list bl,
 	   cvt_optional_eval_for_definition c red_option,
            xlate_formula_opt typ_opt)
   | VernacAssumption (kind, b) ->
-      let b = List.map snd b in (* TODO: handle possible coercions *)
       CT_variable (xlate_var kind, cvt_vernac_binders b)
   | VernacCheckMayEval (None, numopt, c) ->
       CT_check (xlate_formula c)
   | VernacSearch (s,x) ->
+      let translated_restriction = xlate_search_restr x in
       (match s with
 	| SearchPattern c ->
-	    CT_search_pattern(xlate_formula c, xlate_search_restr x)
+	    CT_search_pattern(xlate_formula c, translated_restriction)
 	| SearchHead id ->
-	    CT_search(loc_qualid_to_ct_ID id, xlate_search_restr x)
-	| SearchRewrite c -> xlate_error "TODO: SearchRewrite"
-	| SearchAbout id -> xlate_error "TODO: SearchAbout")
+	    CT_search(loc_qualid_to_ct_ID id, translated_restriction)
+	| SearchRewrite c ->
+	    CT_search_rewrite(xlate_formula c, translated_restriction)
+	| SearchAbout (a::l) ->
+	    let xlate_search_about_item it =
+	      match it with
+		  SearchRef x -> 
+		    CT_coerce_ID_to_ID_OR_STRING(loc_qualid_to_ct_ID x)
+		| SearchString s -> 
+		    CT_coerce_STRING_to_ID_OR_STRING(CT_string s) in
+	    CT_search_about
+	      (CT_id_or_string_ne_list(xlate_search_about_item a,
+				       List.map xlate_search_about_item l),
+	       translated_restriction)
+  	| SearchAbout [] -> assert false)
 
   | (*Record from tactics/Record.v *)
     VernacRecord 
@@ -1660,36 +1719,6 @@ let xlate_vernac =
         xlate_ident s, xlate_binder_list binders, 
 	xlate_formula c1, record_constructor,
          build_record_field_list field_list)
-
-(* TODO
-     | (*Inversions from tactics/Inv.v *)
-       "MakeSemiInversionLemmaFromHyp",
-         ((Varg_int n) :: ((Varg_ident id1) :: ((Varg_ident id2) :: []))) ->
-      CT_derive_inversion
-       (CT_inv_regular, CT_coerce_INT_to_INT_OPT n, id1, id2)
-     | "MakeInversionLemmaFromHyp",
-         ((Varg_int n) :: ((Varg_ident id1) :: ((Varg_ident id2) :: []))) ->
-      CT_derive_inversion
-       (CT_inv_clear,
-       CT_coerce_INT_to_INT_OPT n, id1, id2)
-     | "MakeSemiInversionLemma",
-         ((Varg_ident id) :: (c :: ((Varg_sorttype sort) :: []))) ->
-      CT_derive_inversion_with
-       (CT_inv_regular, id, coerce_iVARG_to_FORMULA c, sort)
-     | "MakeInversionLemma",
-         ((Varg_ident id) :: (c :: ((Varg_sorttype sort) :: []))) ->
-      CT_derive_inversion_with
-       (CT_inv_clear, id,
-       coerce_iVARG_to_FORMULA c, sort)
-     | "MakeDependentSemiInversionLemma",
-         ((Varg_ident id) :: (c :: ((Varg_sorttype sort) :: []))) ->
-      CT_derive_depinversion
-       (CT_inv_regular, id, coerce_iVARG_to_FORMULA c, sort)
-     | "MakeDependentInversionLemma",
-         ((Varg_ident id) :: (c :: ((Varg_sorttype sort) :: []))) ->
-      CT_derive_depinversion
-       (CT_inv_clear, id, coerce_iVARG_to_FORMULA c, sort)
-*)
    | VernacInductive (isind, lmi) ->
       let co_or_ind = if isind then "Inductive" else "CoInductive" in
       let strip_mutind ((_,s), notopt, parameters, c, constructors) =
@@ -1734,54 +1763,70 @@ let xlate_vernac =
 	  (CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi))
    | VernacSyntacticDefinition ((_,id), c, nopt) ->
          CT_syntax_macro (xlate_ident id, xlate_formula c, xlate_int_opt nopt)
-   | VernacRequire (None, spec, lid) -> xlate_error "TODO: Read Module"
-   | VernacRequire (Some impexp, spec, [id]) ->
+   | VernacRequire (impexp, spec, id::idl) ->
       let ct_impexp, ct_spec = get_require_flags impexp spec in
-      CT_require (ct_impexp, ct_spec, loc_qualid_to_ct_ID id,
-        CT_coerce_NONE_to_STRING_OPT CT_none)
-   | VernacRequire (_,_,([]|_::_::_)) ->
-       xlate_error "TODO: general form of future Require"
-   | VernacRequireFrom (Some impexp, spec, filename) ->
-      let ct_impexp, ct_spec = get_require_flags impexp spec 
-      and id = id_of_string (Filename.basename filename)
-      in
-      CT_require
-       (ct_impexp, ct_spec, xlate_ident id, 
-         CT_coerce_STRING_to_STRING_OPT (CT_string filename))
-   | VernacRequireFrom (None, _, _) -> xlate_error "TODO: Read Module"
+      CT_require (ct_impexp, ct_spec, 
+		  CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STRING(
+		  CT_id_ne_list(loc_qualid_to_ct_ID id,
+				List.map loc_qualid_to_ct_ID idl)))
+   | VernacRequire (_,_,[]) ->
+       xlate_error "Require should have at least one id argument"
+   | VernacRequireFrom (impexp, spec, filename) ->
+      let ct_impexp, ct_spec = get_require_flags impexp spec in
+      CT_require(ct_impexp, ct_spec, 
+		 CT_coerce_STRING_to_ID_NE_LIST_OR_STRING(CT_string filename))
 
    | VernacSyntax (phylum, l) -> xlate_error "SYNTAX not implemented"
-       (*Two versions of the syntax node with and without the binder list. *)
-       (*Need to update the metal file and ascent.mli first! 
-         	| ("SYNTAX", [Varg_ident phy; Varg_ident s; spatarg; unparg; blist]) ->
-         	        (syntaxop phy s spatarg unparg blist)
-         	| ("SYNTAX", [Varg_ident phy; Varg_ident s; spatarg; unparg]) ->
-         	        (syntaxop phy s spatarg unparg 
-         coerce_ID_OPT_to_FORMULA_OPT(CT_coerce_NONE_to_ID_OPT(CT_none)))*)
-   | VernacOpenCloseScope sc -> xlate_error "TODO: open/close scope"
-
-   | VernacArgumentsScope _ -> xlate_error "TODO: Arguments Scope"
-
-   | VernacDelimiters _ -> xlate_error "TODO: Delimiters"
-
-   | VernacBindScope _ -> xlate_error "TODO: Bind Scope"
-
-   | VernacNotation _ -> xlate_error "TODO: Notation"
 
+   | VernacOpenCloseScope(true, true, s) -> CT_local_open_scope(CT_ident s)
+   | VernacOpenCloseScope(false, true, s) -> CT_open_scope(CT_ident s)
+   | VernacOpenCloseScope(true, false, s) -> CT_local_close_scope(CT_ident s)
+   | VernacOpenCloseScope(false, false, s) -> CT_close_scope(CT_ident s)
+   | VernacArgumentsScope(qid, l) -> 
+       CT_arguments_scope(loc_qualid_to_ct_ID qid,
+		       CT_id_opt_list
+		       (List.map
+			  (fun x ->
+				  match x with
+				      None -> ctv_ID_OPT_NONE
+				    | Some x -> ctf_ID_OPT_SOME(CT_ident x)) l))
+   | VernacDelimiters(s1,s2) -> CT_delim_scope(CT_ident s1, CT_ident s2)
+   | VernacBindScope(id, a::l) -> 
+       let xlate_class_rawexpr = function
+	   FunClass -> CT_ident "Funclass" | SortClass -> CT_ident "Sortclass"
+	 | RefClass qid -> loc_qualid_to_ct_ID qid in
+       CT_bind_scope(CT_ident id,
+		     CT_id_ne_list(xlate_class_rawexpr a,
+				   List.map xlate_class_rawexpr l))
+   | VernacBindScope(id, []) -> assert false
+   | VernacNotation(b, c, None, _, _) -> assert false
+   | VernacNotation(b, c, Some(s,modif_list), _, opt_scope) -> 
+       let translated_s = CT_string s in
+       let formula = xlate_formula c in
+       let translated_modif_list = 
+	 CT_modifier_list(List.map xlate_syntax_modifier modif_list) in
+       let translated_scope = match opt_scope with
+	   None -> ctv_ID_OPT_NONE
+	 | Some x -> ctf_ID_OPT_SOME(CT_ident x) in
+       if b then
+       CT_local_define_notation
+	 (translated_s, formula, translated_modif_list, translated_scope)
+       else
+	 CT_define_notation(translated_s, formula, 
+			    translated_modif_list, translated_scope)
    | VernacSyntaxExtension _ -> xlate_error "Syntax Extension not implemented"
 
-   | VernacInfix (false,(str,modl),id,_,None) ->
-       (match Metasyntax.interp_infix_modifiers modl with
-	 | (str_assoc,Some n,false,None) ->
-      CT_infix (
-       (match str_assoc with
-        | Some Gramext.LeftA -> CT_lefta
-        | Some Gramext.RightA -> CT_righta
-        | Some Gramext.NonA -> CT_nona
-        | None -> CT_coerce_NONE_to_ASSOC CT_none),
-       CT_int n, CT_string str, loc_qualid_to_ct_ID id)
-	 | _ -> xlate_error "TODO: handle onlyparse and format")
-   | VernacInfix _ -> xlate_error "TODO: handle scopes and locality"
+   | VernacInfix (b,(str,modl),id,_, opt_scope) ->
+       let id1 = loc_qualid_to_ct_ID id in
+       let modl1 = CT_modifier_list(List.map xlate_syntax_modifier modl) in
+       let s = CT_string str in
+       let translated_scope = match opt_scope with
+	   None -> ctv_ID_OPT_NONE
+	 | Some x -> ctf_ID_OPT_SOME(CT_ident x) in
+	 if b then
+	   CT_local_infix(s, id1,modl1, translated_scope)
+	 else
+	   CT_infix(s, id1,modl1, translated_scope)
    | VernacGrammar _ -> xlate_error "GRAMMAR not implemented"
    | VernacCoercion (s, id1, id2, id3) ->
       let id_opt = CT_coerce_NONE_to_IDENTITY_OPT CT_none in
@@ -1807,9 +1852,13 @@ let xlate_vernac =
   | VernacExtend (s, l) ->
       CT_user_vernac
        (CT_ident s, CT_varg_list (List.map coerce_genarg_to_VARG l))
-  | VernacDebug b -> xlate_error "TODO: Debug On/Off"
-
-  | (VernacList _ | VernacV7only _ | VernacV8only _) ->
+  | VernacDebug b -> xlate_error "Debug On/Off not supported"
+  | VernacList((_, a)::l) -> 
+      CT_coerce_COMMAND_LIST_to_COMMAND
+	(CT_command_list(xlate_vernac a, 
+			 List.map (fun (_, x) -> xlate_vernac x) l))
+  | VernacList([]) -> assert false
+  | (VernacV7only _ | VernacV8only _) ->
       xlate_error "Not treated here"
   | VernacNop -> CT_proof_no_op
   | VernacComments l -> 
@@ -1818,16 +1867,24 @@ let xlate_vernac =
       CT_implicits
 	(reference_to_ct_ID id,
 	 match opt_positions with
-	     None -> CT_int_list[]
+	     None -> CT_id_list[]
 	   | Some l -> 
-	       CT_int_list
-	       (List.map (function ExplByPos x -> CT_int x | ExplByName _ ->
-		 xlate_error "TODO: explicit argument by name") l))
-  | VernacReserve _ -> xlate_error "TODO: Default Variable Type"
+	       CT_id_list
+	       (List.map
+		  (function ExplByPos x
+		       -> xlate_error
+			   "explication argument by rank is obsolete"
+		     | ExplByName id -> CT_ident (string_of_id id)) l))
+  | VernacReserve((_,a)::l, f) ->
+      CT_reserve(CT_id_ne_list(xlate_ident a, 
+			       List.map (fun (_,x) -> xlate_ident x) l),
+		 xlate_formula f)
+  | VernacReserve([], _) -> assert false
   | VernacLocate(LocateTerm id) -> CT_locate(reference_to_ct_ID id)
   | VernacLocate(LocateLibrary id) -> CT_locate_lib(reference_to_ct_ID id)
   | VernacLocate(LocateFile s) -> CT_locate_file(CT_string s)
-  | VernacLocate(LocateNotation _) -> xlate_error "TODO: Locate Notation"
+  | VernacLocate(LocateNotation s) -> CT_locate_notation(CT_string s)
+  | VernacTime(v) -> CT_time(xlate_vernac v)
   | VernacSetOption (Goptions.SecondaryTable ("Implicit", "Arguments"), BoolValue true)->CT_user_vernac (CT_ident "IMPLICIT_ARGS_ON", CT_varg_list[])
   | (VernacGlobalCheck _|VernacPrintOption _|
      VernacMemOption (_, _)|VernacRemoveOption (_, _)|VernacAddOption (_, _)|
@@ -1835,7 +1892,7 @@ let xlate_vernac =
      VernacBack _|VernacRestoreState _|
      VernacWriteState _|VernacSolveExistential (_, _)|VernacCanonical _|
      VernacImport (_, _)|VernacExactProof _|VernacDistfix _|
-     VernacTacticGrammar _|VernacVar _|VernacTime _|VernacProof _)
+     VernacTacticGrammar _|VernacVar _|VernacProof _)
     -> xlate_error "TODO: vernac"
 
   (* Modules and Module Types *)