1 files changed, 0 insertions, 795 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
deleted file mode 100644
index 2eb2c381..00000000
--- a/contrib/interface/ascent.mli
+++ /dev/null
@@ -1,795 +0,0 @@
-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_coerce_SINGLE_OPTION_VALUE_to_AST of ct_SINGLE_OPTION_VALUE
-  | CT_astnode of ct_ID * ct_AST_LIST
-  | CT_astpath of ct_ID_LIST
-  | CT_astslam of ct_ID_OPT * ct_AST
-and ct_AST_LIST =
-    CT_ast_list of ct_AST list
-and ct_BINARY =
-    CT_binary of int
-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 =
-    CT_binder_ne_list of ct_BINDER * ct_BINDER list
-and ct_BINDING =
-    CT_binding of ct_ID_OR_INT * ct_FORMULA
-and ct_BINDING_LIST =
-    CT_binding_list of ct_BINDING list
-and t_BOOL =
-    CT_false
-  | CT_true
-and ct_CASE =
-    CT_case of string
-and ct_CLAUSE =
-    CT_clause of ct_HYP_LOCATION_LIST_OR_STAR * ct_STAR_OPT
-and ct_COERCION_OPT =
-    CT_coerce_NONE_to_COERCION_OPT of ct_NONE
-  | CT_coercion_atm
-and ct_COFIXTAC =
-    CT_cofixtac of ct_ID * ct_FORMULA
-and ct_COFIX_REC =
-    CT_cofix_rec of ct_ID * ct_BINDER_LIST * ct_FORMULA * ct_FORMULA
-and ct_COFIX_REC_LIST =
-    CT_cofix_rec_list of ct_COFIX_REC * ct_COFIX_REC list
-and ct_COFIX_TAC_LIST =
-    CT_cofix_tac_list of ct_COFIXTAC 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_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_field of ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA_OPT
-  | 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_declare_module of ct_ID * ct_MODULE_BINDER_LIST * ct_MODULE_TYPE_CHECK * ct_MODULE_EXPR
-  | 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_extract_to_file of ct_STRING * ct_ID_NE_LIST
-  | CT_extraction of ct_ID_OPT
-  | CT_fix_decl of ct_FIX_REC_LIST
-  | CT_focus of ct_INT_OPT
-  | CT_go of ct_INT_OR_LOCN
-  | CT_guarded
-  | CT_hint_destruct of ct_ID * ct_INT * ct_DESTRUCT_LOCATION * ct_FORMULA * ct_TACTIC_COM * ct_ID_LIST
-  | CT_hint_extern of ct_INT * ct_FORMULA_OPT * 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_hints_immediate of ct_FORMULA_NE_LIST * ct_ID_LIST
-  | CT_hints_resolve of ct_FORMULA_NE_LIST * ct_ID_LIST
-  | CT_hyp_search_pattern of ct_FORMULA * ct_IN_OR_OUT_MODULES
-  | CT_implicits of ct_ID * ct_ID_LIST_OPT
-  | CT_import_id of ct_ID_NE_LIST
-  | CT_ind_scheme of ct_SCHEME_SPEC_LIST
-  | CT_infix of ct_STRING * ct_ID * ct_MODIFIER_LIST * ct_ID_OPT
-  | CT_inline of ct_ID_NE_LIST
-  | 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_hints_immediate of ct_FORMULA_NE_LIST * ct_ID_LIST
-  | CT_local_hints_resolve of ct_FORMULA_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_local_reserve_notation of ct_STRING * ct_MODIFIER_LIST
-  | 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
-  | CT_ml_print_modules
-  | CT_ml_print_path
-  | CT_module of ct_ID * ct_MODULE_BINDER_LIST * ct_MODULE_TYPE_CHECK * ct_MODULE_EXPR
-  | CT_module_type_decl of ct_ID * ct_MODULE_BINDER_LIST * ct_MODULE_TYPE_OPT
-  | CT_no_inline of ct_ID_NE_LIST
-  | CT_omega_flag of ct_OMEGA_MODE * ct_OMEGA_FEATURE
-  | CT_open_scope of ct_ID
-  | CT_print
-  | CT_print_about of ct_ID
-  | CT_print_all
-  | CT_print_classes
-  | CT_print_ltac of ct_ID
-  | 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_OR_STAR
-  | CT_print_rewrite_hintdb of ct_ID
-  | 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_setoids
-  | 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_proof_with of ct_TACTIC_COM
-  | CT_pwd
-  | CT_quit
-  | CT_read_module of ct_ID
-  | CT_rec_ml_add_path of ct_STRING
-  | 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_NE_LIST_OR_STRING
-  | CT_reserve of ct_ID_NE_LIST * ct_FORMULA
-  | CT_reserve_notation of ct_STRING * ct_MODIFIER_LIST
-  | CT_reset of ct_ID
-  | CT_reset_section of ct_ID
-  | CT_restart
-  | CT_restore_state of ct_ID
-  | CT_resume of ct_ID_OPT
-  | 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
-  | CT_section_struct of ct_SECTION_BEGIN * ct_SECTION_BODY * ct_COMMAND
-  | CT_set_natural of ct_ID
-  | CT_set_natural_default
-  | CT_set_option of ct_TABLE
-  | CT_set_option_value of ct_TABLE * ct_SINGLE_OPTION_VALUE
-  | CT_set_option_value2 of ct_TABLE * ct_ID_OR_STRING_NE_LIST
-  | CT_sethyp of ct_INT
-  | CT_setundo of ct_INT
-  | CT_show_existentials
-  | CT_show_goal of ct_INT_OPT
-  | CT_show_implicit of ct_INT
-  | CT_show_intro
-  | CT_show_intros
-  | CT_show_node
-  | CT_show_proof
-  | CT_show_proofs
-  | CT_show_script
-  | CT_show_tree
-  | CT_solve of ct_INT * ct_TACTIC_COM * ct_DOTDOT_OPT
-  | CT_strategy of ct_LEVEL_LIST
-  | CT_suspend
-  | CT_syntax_macro of ct_ID * ct_FORMULA * ct_INT_OPT
-  | CT_tactic_definition of ct_TAC_DEF_NE_LIST
-  | CT_test_natural_feature of ct_NATURAL_FEATURE * ct_ID
-  | CT_theorem_struct of ct_THEOREM_GOAL * ct_PROOF_SCRIPT
-  | CT_time of ct_COMMAND
-  | CT_undo of ct_INT_OPT
-  | CT_unfocus
-  | CT_unset_option of ct_TABLE
-  | CT_unsethyp
-  | CT_unsetundo
-  | CT_user_vernac of ct_ID * ct_VARG_LIST
-  | CT_variable of ct_VAR * ct_BINDER_NE_LIST
-  | CT_write_module of ct_ID * ct_STRING_OPT
-and ct_LEVEL_LIST =
-    CT_level_list of (ct_LEVEL * ct_ID_LIST) list
-and ct_LEVEL =
-    CT_Opaque
-  | CT_Level of ct_INT
-  | CT_Expand
-and ct_COMMAND_LIST =
-    CT_command_list of ct_COMMAND * ct_COMMAND list
-and ct_COMMENT =
-    CT_comment of string
-and ct_COMMENT_S =
-    CT_comment_s of ct_COMMENT list
-and ct_CONSTR =
-    CT_constr of ct_ID * ct_FORMULA
-  | CT_constr_coercion of ct_ID * ct_FORMULA
-and ct_CONSTR_LIST =
-    CT_constr_list of ct_CONSTR list
-and ct_CONTEXT_HYP_LIST =
-    CT_context_hyp_list of ct_PREMISE_PATTERN list
-and ct_CONTEXT_PATTERN =
-    CT_coerce_FORMULA_to_CONTEXT_PATTERN of ct_FORMULA
-  | CT_context of ct_ID_OPT * ct_FORMULA
-and ct_CONTEXT_RULE =
-    CT_context_rule of ct_CONTEXT_HYP_LIST * ct_CONTEXT_PATTERN * ct_TACTIC_COM
-  | CT_def_context_rule of ct_TACTIC_COM
-and ct_CONVERSION_FLAG =
-    CT_beta
-  | CT_delta
-  | CT_evar
-  | CT_iota
-  | CT_zeta
-and ct_CONVERSION_FLAG_LIST =
-    CT_conversion_flag_list of ct_CONVERSION_FLAG list
-and ct_CONV_SET =
-    CT_unf of ct_ID list
-  | CT_unfbut of ct_ID list
-and ct_CO_IND =
-    CT_co_ind of string
-and ct_DECL_NOTATION_OPT =
-    CT_coerce_NONE_to_DECL_NOTATION_OPT of ct_NONE
-  | CT_decl_notation of ct_STRING * ct_FORMULA * ct_ID_OPT
-and ct_DEF =
-    CT_def of ct_ID_OPT * ct_FORMULA
-and ct_DEFN =
-    CT_defn of string
-and ct_DEFN_OR_THM =
-    CT_coerce_DEFN_to_DEFN_OR_THM of ct_DEFN
-  | CT_coerce_THM_to_DEFN_OR_THM of ct_THM
-and ct_DEF_BODY =
-    CT_coerce_CONTEXT_PATTERN_to_DEF_BODY of ct_CONTEXT_PATTERN
-  | CT_coerce_EVAL_CMD_to_DEF_BODY of ct_EVAL_CMD
-  | CT_type_of of ct_FORMULA
-and ct_DEF_BODY_OPT =
-    CT_coerce_DEF_BODY_to_DEF_BODY_OPT of ct_DEF_BODY
-  | CT_coerce_FORMULA_OPT_to_DEF_BODY_OPT of ct_FORMULA_OPT
-and ct_DEP =
-    CT_dep of string
-and ct_DESTRUCTING =
-    CT_coerce_NONE_to_DESTRUCTING of ct_NONE
-  | CT_destructing
-and ct_DESTRUCT_LOCATION =
-    CT_conclusion_location
-  | CT_discardable_hypothesis
-  | CT_hypothesis_location
-and ct_DOTDOT_OPT =
-    CT_coerce_NONE_to_DOTDOT_OPT of ct_NONE
-  | CT_dotdot
-and ct_EQN =
-    CT_eqn of ct_MATCH_PATTERN_NE_LIST * ct_FORMULA
-and ct_EQN_LIST =
-    CT_eqn_list of ct_EQN list
-and ct_EVAL_CMD =
-    CT_eval of ct_INT_OPT * ct_RED_COM * ct_FORMULA
-and ct_FIXTAC =
-    CT_fixtac of ct_ID * ct_INT * ct_FORMULA
-and ct_FIX_BINDER =
-    CT_coerce_FIX_REC_to_FIX_BINDER of ct_FIX_REC
-  | CT_fix_binder of ct_ID * ct_INT * ct_FORMULA * ct_FORMULA
-and ct_FIX_BINDER_LIST =
-    CT_fix_binder_list of ct_FIX_BINDER * ct_FIX_BINDER list
-and ct_FIX_REC =
-    CT_fix_rec of ct_ID * ct_BINDER_NE_LIST * ct_ID_OPT *
-      ct_FORMULA * ct_FORMULA
-and ct_FIX_REC_LIST =
-    CT_fix_rec_list of ct_FIX_REC * ct_FIX_REC list
-and ct_FIX_TAC_LIST =
-    CT_fix_tac_list of ct_FIXTAC list
-and ct_FORMULA =
-    CT_coerce_BINARY_to_FORMULA of ct_BINARY
-  | CT_coerce_ID_to_FORMULA of ct_ID
-  | CT_coerce_NUM_to_FORMULA of ct_NUM
-  | CT_coerce_SORT_TYPE_to_FORMULA of ct_SORT_TYPE
-  | CT_coerce_TYPED_FORMULA_to_FORMULA of ct_TYPED_FORMULA
-  | CT_appc of ct_FORMULA * ct_FORMULA_NE_LIST
-  | CT_arrowc of ct_FORMULA * ct_FORMULA
-  | CT_bang of ct_FORMULA
-  | CT_cases of ct_MATCHED_FORMULA_NE_LIST * ct_FORMULA_OPT * ct_EQN_LIST
-  | CT_cofixc of ct_ID * ct_COFIX_REC_LIST
-  | CT_elimc of ct_CASE * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA_LIST
-  | CT_existvarc
-  | CT_fixc of ct_ID * ct_FIX_BINDER_LIST
-  | CT_if of ct_FORMULA * ct_RETURN_INFO * ct_FORMULA * ct_FORMULA
-  | CT_inductive_let of ct_FORMULA_OPT * ct_ID_OPT_NE_LIST * ct_FORMULA * ct_FORMULA
-  | CT_labelled_arg of ct_ID * ct_FORMULA
-  | CT_lambdac of ct_BINDER_NE_LIST * ct_FORMULA
-  | CT_let_tuple of ct_ID_OPT_NE_LIST * ct_RETURN_INFO * ct_FORMULA * ct_FORMULA
-  | CT_letin of ct_DEF * ct_FORMULA
-  | CT_notation of ct_STRING * ct_FORMULA_LIST
-  | CT_num_encapsulator of ct_NUM_TYPE * ct_FORMULA
-  | CT_prodc of ct_BINDER_NE_LIST * ct_FORMULA
-  | CT_proj of ct_FORMULA * ct_FORMULA_NE_LIST
-and ct_FORMULA_LIST =
-    CT_formula_list of ct_FORMULA list
-and ct_FORMULA_NE_LIST =
-    CT_formula_ne_list of ct_FORMULA * ct_FORMULA list
-and ct_FORMULA_OPT =
-    CT_coerce_FORMULA_to_FORMULA_OPT of ct_FORMULA
-  | CT_coerce_ID_OPT_to_FORMULA_OPT of ct_ID_OPT
-and ct_FORMULA_OR_INT =
-    CT_coerce_FORMULA_to_FORMULA_OR_INT of ct_FORMULA
-  | CT_coerce_ID_OR_INT_to_FORMULA_OR_INT of ct_ID_OR_INT
-and ct_GRAMMAR =
-    CT_grammar_none
-and ct_HYP_LOCATION =
-    CT_coerce_UNFOLD_to_HYP_LOCATION of ct_UNFOLD
-  | CT_intype of ct_ID * ct_INT_LIST
-  | CT_invalue of ct_ID * ct_INT_LIST
-and ct_HYP_LOCATION_LIST_OR_STAR =
-    CT_coerce_STAR_to_HYP_LOCATION_LIST_OR_STAR of ct_STAR
-  | CT_hyp_location_list of ct_HYP_LOCATION list
-and ct_ID =
-    CT_ident of string
-  | CT_metac of ct_INT
-  | CT_metaid of string
-and ct_IDENTITY_OPT =
-    CT_coerce_NONE_to_IDENTITY_OPT of ct_NONE
-  | CT_identity
-and ct_ID_LIST =
-    CT_id_list of ct_ID list
-and ct_ID_LIST_LIST =
-    CT_id_list_list of ct_ID_LIST list
-and ct_ID_LIST_OPT =
-    CT_coerce_ID_LIST_to_ID_LIST_OPT of ct_ID_LIST
-  | CT_coerce_NONE_to_ID_LIST_OPT of ct_NONE
-and ct_ID_NE_LIST =
-    CT_id_ne_list of ct_ID * ct_ID 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 =
-    CT_coerce_ID_OPT_to_ID_OPT_OR_ALL of ct_ID_OPT
-  | CT_all
-and ct_ID_OR_INT =
-    CT_coerce_ID_to_ID_OR_INT of ct_ID
-  | CT_coerce_INT_to_ID_OR_INT of ct_INT
-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_IMPEXP =
-    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
-and ct_IND_SPEC_LIST =
-    CT_ind_spec_list of ct_IND_SPEC list
-and ct_INT =
-    CT_int of int
-and ct_INTRO_PATT =
-    CT_coerce_ID_to_INTRO_PATT of ct_ID
-  | CT_disj_pattern of ct_INTRO_PATT_LIST * ct_INTRO_PATT_LIST list
-and ct_INTRO_PATT_LIST =
-    CT_intro_patt_list of ct_INTRO_PATT list
-and ct_INTRO_PATT_OPT =
-    CT_coerce_ID_OPT_to_INTRO_PATT_OPT of ct_ID_OPT
-  | CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT of ct_INTRO_PATT
-and ct_INT_LIST =
-    CT_int_list of ct_INT list
-and ct_INT_NE_LIST =
-    CT_int_ne_list of ct_INT * ct_INT list
-and ct_INT_OPT =
-    CT_coerce_INT_to_INT_OPT of ct_INT
-  | CT_coerce_NONE_to_INT_OPT of ct_NONE
-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
-  | CT_inv_simple
-and ct_IN_OR_OUT_MODULES =
-    CT_coerce_NONE_to_IN_OR_OUT_MODULES of ct_NONE
-  | CT_in_modules of ct_ID_NE_LIST
-  | CT_out_modules of ct_ID_NE_LIST
-and ct_LET_CLAUSE =
-    CT_let_clause of ct_ID * ct_TACTIC_OPT * ct_LET_VALUE
-and ct_LET_CLAUSES =
-    CT_let_clauses of ct_LET_CLAUSE * ct_LET_CLAUSE list
-and ct_LET_VALUE =
-    CT_coerce_DEF_BODY_to_LET_VALUE of ct_DEF_BODY
-  | CT_coerce_TACTIC_COM_to_LET_VALUE of ct_TACTIC_COM
-and ct_LOCAL_OPT =
-    CT_coerce_NONE_to_LOCAL_OPT of ct_NONE
-  | CT_local
-and ct_LOCN =
-    CT_locn of string
-and ct_MATCHED_FORMULA =
-    CT_coerce_FORMULA_to_MATCHED_FORMULA of ct_FORMULA
-  | CT_formula_as of ct_FORMULA * ct_ID_OPT
-  | CT_formula_as_in of ct_FORMULA * ct_ID_OPT * ct_FORMULA
-  | CT_formula_in of ct_FORMULA * ct_FORMULA
-and ct_MATCHED_FORMULA_NE_LIST =
-    CT_matched_formula_ne_list of ct_MATCHED_FORMULA * ct_MATCHED_FORMULA list
-and ct_MATCH_PATTERN =
-    CT_coerce_ID_OPT_to_MATCH_PATTERN of ct_ID_OPT
-  | CT_coerce_NUM_to_MATCH_PATTERN of ct_NUM
-  | CT_pattern_app of ct_MATCH_PATTERN * ct_MATCH_PATTERN_NE_LIST
-  | CT_pattern_as of ct_MATCH_PATTERN * ct_ID_OPT
-  | CT_pattern_delimitors of ct_NUM_TYPE * ct_MATCH_PATTERN
-  | CT_pattern_notation of ct_STRING * ct_MATCH_PATTERN_LIST
-and ct_MATCH_PATTERN_LIST =
-    CT_match_pattern_list of ct_MATCH_PATTERN list
-and ct_MATCH_PATTERN_NE_LIST =
-    CT_match_pattern_ne_list of ct_MATCH_PATTERN * ct_MATCH_PATTERN list
-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_MODULE_BINDER =
-    CT_module_binder of ct_ID_NE_LIST * ct_MODULE_TYPE
-and ct_MODULE_BINDER_LIST =
-    CT_module_binder_list of ct_MODULE_BINDER list
-and ct_MODULE_EXPR =
-    CT_coerce_ID_OPT_to_MODULE_EXPR of ct_ID_OPT
-  | CT_module_app of ct_MODULE_EXPR * ct_MODULE_EXPR
-and ct_MODULE_TYPE =
-    CT_coerce_ID_to_MODULE_TYPE of ct_ID
-  | CT_module_type_with_def of ct_MODULE_TYPE * ct_ID_LIST * ct_FORMULA
-  | CT_module_type_with_mod of ct_MODULE_TYPE * ct_ID_LIST * ct_ID
-and ct_MODULE_TYPE_CHECK =
-    CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK of ct_MODULE_TYPE_OPT
-  | CT_only_check of ct_MODULE_TYPE
-and ct_MODULE_TYPE_OPT =
-    CT_coerce_ID_OPT_to_MODULE_TYPE_OPT of ct_ID_OPT
-  | CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT of ct_MODULE_TYPE
-and ct_NATURAL_FEATURE =
-    CT_contractible
-  | CT_implicit
-  | CT_nat_transparent
-and ct_NONE =
-    CT_none
-and ct_NUM =
-    CT_int_encapsulator of string
-and ct_NUM_TYPE =
-    CT_num_type of string
-and ct_OMEGA_FEATURE =
-    CT_coerce_STRING_to_OMEGA_FEATURE of ct_STRING
-  | CT_flag_action
-  | CT_flag_system
-  | CT_flag_time
-and ct_OMEGA_MODE =
-    CT_set
-  | CT_switch
-  | CT_unset
-and ct_ORIENTATION =
-    CT_lr
-  | CT_rl
-and ct_PATTERN =
-    CT_pattern_occ of ct_INT_LIST * ct_FORMULA
-and ct_PATTERN_NE_LIST =
-    CT_pattern_ne_list of ct_PATTERN * ct_PATTERN list
-and ct_PATTERN_OPT =
-    CT_coerce_NONE_to_PATTERN_OPT of ct_NONE
-  | CT_coerce_PATTERN_to_PATTERN_OPT of ct_PATTERN
-and ct_PREMISE =
-    CT_coerce_TYPED_FORMULA_to_PREMISE of ct_TYPED_FORMULA
-  | CT_eval_result of ct_FORMULA * ct_FORMULA * ct_FORMULA
-  | CT_premise of ct_ID * ct_FORMULA
-and ct_PREMISES_LIST =
-    CT_premises_list of ct_PREMISE list
-and ct_PREMISE_PATTERN =
-    CT_premise_pattern of ct_ID_OPT * ct_CONTEXT_PATTERN
-and ct_PROOF_SCRIPT =
-    CT_proof_script of ct_COMMAND list
-and ct_RECCONSTR =
-    CT_defrecconstr of ct_ID_OPT * ct_FORMULA * ct_FORMULA_OPT
-  | CT_defrecconstr_coercion of ct_ID_OPT * ct_FORMULA * ct_FORMULA_OPT
-  | CT_recconstr of ct_ID_OPT * ct_FORMULA
-  | CT_recconstr_coercion of ct_ID_OPT * ct_FORMULA
-and ct_RECCONSTR_LIST =
-    CT_recconstr_list of ct_RECCONSTR list
-and ct_REC_TACTIC_FUN =
-    CT_rec_tactic_fun of ct_ID * ct_ID_OPT_NE_LIST * ct_TACTIC_COM
-and ct_REC_TACTIC_FUN_LIST =
-    CT_rec_tactic_fun_list of ct_REC_TACTIC_FUN * ct_REC_TACTIC_FUN list
-and ct_RED_COM =
-    CT_cbv of ct_CONVERSION_FLAG_LIST * ct_CONV_SET
-  | CT_fold of ct_FORMULA_LIST
-  | CT_hnf
-  | CT_lazy of ct_CONVERSION_FLAG_LIST * ct_CONV_SET
-  | CT_pattern of ct_PATTERN_NE_LIST
-  | CT_red
-  | CT_cbvvm
-  | CT_simpl of ct_PATTERN_OPT
-  | CT_unfold of ct_UNFOLD_NE_LIST
-and ct_RETURN_INFO =
-    CT_coerce_NONE_to_RETURN_INFO of ct_NONE
-  | CT_as_and_return of ct_ID_OPT * ct_FORMULA
-  | CT_return of ct_FORMULA
-and ct_RULE =
-    CT_rule of ct_PREMISES_LIST * ct_FORMULA
-and ct_RULE_LIST =
-    CT_rule_list of ct_RULE list
-and ct_SCHEME_SPEC =
-    CT_scheme_spec of ct_ID * ct_DEP * ct_FORMULA * ct_SORT_TYPE
-and ct_SCHEME_SPEC_LIST =
-    CT_scheme_spec_list of ct_SCHEME_SPEC * ct_SCHEME_SPEC list
-and ct_SCOMMENT_CONTENT =
-    CT_coerce_FORMULA_to_SCOMMENT_CONTENT of ct_FORMULA
-  | CT_coerce_ID_OR_STRING_to_SCOMMENT_CONTENT of ct_ID_OR_STRING
-and ct_SCOMMENT_CONTENT_LIST =
-    CT_scomment_content_list of ct_SCOMMENT_CONTENT list
-and ct_SECTION_BEGIN =
-    CT_section of ct_ID
-and ct_SECTION_BODY =
-    CT_section_body of ct_COMMAND list
-and ct_SIGNED_INT =
-    CT_coerce_INT_to_SIGNED_INT of ct_INT
-  | CT_minus of ct_INT
-and ct_SIGNED_INT_LIST =
-    CT_signed_int_list of ct_SIGNED_INT list
-and ct_SINGLE_OPTION_VALUE =
-    CT_coerce_INT_to_SINGLE_OPTION_VALUE of ct_INT
-  | CT_coerce_STRING_to_SINGLE_OPTION_VALUE of ct_STRING
-and ct_SORT_TYPE =
-    CT_sortc of string
-and ct_SPEC_LIST =
-    CT_coerce_BINDING_LIST_to_SPEC_LIST of ct_BINDING_LIST
-  | CT_coerce_FORMULA_LIST_to_SPEC_LIST of ct_FORMULA_LIST
-and ct_SPEC_OPT =
-    CT_coerce_NONE_to_SPEC_OPT of ct_NONE
-  | CT_spec
-and ct_STAR =
-    CT_star
-and ct_STAR_OPT =
-    CT_coerce_NONE_to_STAR_OPT of ct_NONE
-  | CT_coerce_STAR_to_STAR_OPT of ct_STAR
-and ct_STRING =
-    CT_string of string
-and ct_STRING_NE_LIST =
-    CT_string_ne_list of ct_STRING * ct_STRING list
-and ct_STRING_OPT =
-    CT_coerce_NONE_to_STRING_OPT of ct_NONE
-  | CT_coerce_STRING_to_STRING_OPT of ct_STRING
-and ct_TABLE =
-    CT_coerce_ID_to_TABLE of ct_ID
-  | CT_table of ct_ID * ct_ID
-and ct_TACTIC_ARG =
-    CT_coerce_EVAL_CMD_to_TACTIC_ARG of ct_EVAL_CMD
-  | CT_coerce_FORMULA_OR_INT_to_TACTIC_ARG of ct_FORMULA_OR_INT
-  | CT_coerce_TACTIC_COM_to_TACTIC_ARG of ct_TACTIC_COM
-  | CT_coerce_TERM_CHANGE_to_TACTIC_ARG of ct_TERM_CHANGE
-  | CT_void
-and ct_TACTIC_ARG_LIST =
-    CT_tactic_arg_list of ct_TACTIC_ARG * ct_TACTIC_ARG list
-and ct_TACTIC_COM =
-    CT_abstract of ct_ID_OPT * ct_TACTIC_COM
-  | CT_absurd of ct_FORMULA
-  | CT_any_constructor of ct_TACTIC_OPT
-  | CT_apply of ct_FORMULA * ct_SPEC_LIST
-  | CT_assert of ct_ID_OPT * ct_FORMULA
-  | CT_assumption
-  | CT_auto of ct_INT_OPT
-  | CT_auto_with of ct_INT_OPT * ct_ID_NE_LIST_OR_STAR
-  | CT_autorewrite of ct_ID_NE_LIST * ct_TACTIC_OPT
-  | CT_autotdb of ct_INT_OPT
-  | CT_case_type of ct_FORMULA
-  | CT_casetac of ct_FORMULA * ct_SPEC_LIST
-  | CT_cdhyp of ct_ID
-  | CT_change of ct_FORMULA * ct_CLAUSE
-  | CT_change_local of ct_PATTERN * ct_FORMULA * ct_CLAUSE
-  | CT_clear of ct_ID_NE_LIST
-  | CT_clear_body of ct_ID_NE_LIST
-  | CT_cofixtactic of ct_ID_OPT * ct_COFIX_TAC_LIST
-  | CT_condrewrite_lr of ct_TACTIC_COM * ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT
-  | CT_condrewrite_rl of ct_TACTIC_COM * ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT
-  | CT_constructor of ct_INT * ct_SPEC_LIST
-  | CT_contradiction
-  | CT_contradiction_thm of ct_FORMULA * ct_SPEC_LIST
-  | CT_cut of ct_FORMULA
-  | CT_cutrewrite_lr of ct_FORMULA * ct_ID_OPT
-  | CT_cutrewrite_rl of ct_FORMULA * ct_ID_OPT
-  | CT_dauto of ct_INT_OPT * ct_INT_OPT
-  | CT_dconcl
-  | CT_decompose_list of ct_ID_NE_LIST * ct_FORMULA
-  | CT_decompose_record of ct_FORMULA
-  | CT_decompose_sum of ct_FORMULA
-  | CT_depinversion of ct_INV_TYPE * ct_ID_OR_INT * ct_INTRO_PATT_OPT * ct_FORMULA_OPT
-  | CT_deprewrite_lr of ct_ID
-  | CT_deprewrite_rl of ct_ID
-  | CT_destruct of ct_ID_OR_INT
-  | CT_dhyp of ct_ID
-  | CT_discriminate_eq of ct_ID_OR_INT_OPT
-  | CT_do of ct_ID_OR_INT * ct_TACTIC_COM
-  | CT_eapply of ct_FORMULA * ct_SPEC_LIST
-  | CT_eauto of ct_ID_OR_INT_OPT * ct_ID_OR_INT_OPT
-  | CT_eauto_with of ct_ID_OR_INT_OPT * ct_ID_OR_INT_OPT * ct_ID_NE_LIST_OR_STAR
-  | CT_elim of ct_FORMULA * ct_SPEC_LIST * ct_USING
-  | CT_elim_type of ct_FORMULA
-  | CT_exact of ct_FORMULA
-  | CT_exact_no_check of ct_FORMULA
-  | CT_vm_cast_no_check of ct_FORMULA
-  | CT_exists of ct_SPEC_LIST
-  | CT_fail of ct_ID_OR_INT * ct_STRING_OPT
-  | CT_first of ct_TACTIC_COM * ct_TACTIC_COM list
-  | CT_firstorder of ct_TACTIC_OPT
-  | CT_firstorder_using of ct_TACTIC_OPT * ct_ID_NE_LIST
-  | CT_firstorder_with of ct_TACTIC_OPT * ct_ID_NE_LIST
-  | CT_fixtactic of ct_ID_OPT * ct_INT * ct_FIX_TAC_LIST
-  | CT_formula_marker of ct_FORMULA
-  | CT_fresh of ct_STRING_OPT
-  | CT_generalize of ct_FORMULA_NE_LIST
-  | CT_generalize_dependent of ct_FORMULA
-  | CT_idtac of ct_STRING_OPT
-  | CT_induction of ct_ID_OR_INT
-  | CT_info of ct_TACTIC_COM
-  | CT_injection_eq of ct_ID_OR_INT_OPT
-  | CT_instantiate of ct_INT * ct_FORMULA * ct_CLAUSE
-  | CT_intro of ct_ID_OPT
-  | CT_intro_after of ct_ID_OPT * ct_ID
-  | CT_intros of ct_INTRO_PATT_LIST
-  | CT_intros_until of ct_ID_OR_INT
-  | CT_inversion of ct_INV_TYPE * ct_ID_OR_INT * ct_INTRO_PATT_OPT * ct_ID_LIST
-  | CT_left of ct_SPEC_LIST
-  | CT_let_ltac of ct_LET_CLAUSES * ct_LET_VALUE
-  | CT_lettac of ct_ID_OPT * ct_FORMULA * ct_CLAUSE
-  | CT_match_context of ct_CONTEXT_RULE * ct_CONTEXT_RULE list
-  | CT_match_context_reverse of ct_CONTEXT_RULE * ct_CONTEXT_RULE list
-  | CT_match_tac of ct_TACTIC_COM * ct_MATCH_TAC_RULES
-  | CT_move_after of ct_ID * ct_ID
-  | CT_new_destruct of ct_FORMULA_OR_INT list * ct_USING * ct_INTRO_PATT_OPT
-  | CT_new_induction of ct_FORMULA_OR_INT list * ct_USING * ct_INTRO_PATT_OPT
-  | CT_omega
-  | CT_orelse of ct_TACTIC_COM * ct_TACTIC_COM
-  | CT_parallel of ct_TACTIC_COM * ct_TACTIC_COM list
-  | CT_pose of ct_ID_OPT * ct_FORMULA
-  | CT_progress of ct_TACTIC_COM
-  | CT_prolog of ct_FORMULA_LIST * ct_INT
-  | CT_rec_tactic_in of ct_REC_TACTIC_FUN_LIST * ct_TACTIC_COM
-  | CT_reduce of ct_RED_COM * ct_CLAUSE
-  | CT_refine of ct_FORMULA
-  | CT_reflexivity
-  | CT_rename of ct_ID * ct_ID
-  | CT_repeat of ct_TACTIC_COM
-  | CT_replace_with of ct_FORMULA * ct_FORMULA * ct_CLAUSE * ct_TACTIC_OPT
-  | CT_rewrite_lr of ct_FORMULA * ct_SPEC_LIST * ct_CLAUSE
-  | CT_rewrite_rl of ct_FORMULA * ct_SPEC_LIST * ct_CLAUSE
-  | CT_right of ct_SPEC_LIST
-  | CT_ring of ct_FORMULA_LIST
-  | CT_simple_user_tac of ct_ID * ct_TACTIC_ARG_LIST
-  | CT_simplify_eq of ct_ID_OR_INT_OPT
-  | CT_specialize of ct_INT_OPT * ct_FORMULA * ct_SPEC_LIST
-  | CT_split of ct_SPEC_LIST
-  | CT_subst of ct_ID_LIST
-  | CT_superauto of ct_INT_OPT * ct_ID_LIST * ct_DESTRUCTING * ct_USINGTDB
-  | CT_symmetry of ct_CLAUSE
-  | CT_tac_double of ct_ID_OR_INT * ct_ID_OR_INT
-  | CT_tacsolve of ct_TACTIC_COM * ct_TACTIC_COM list
-  | CT_tactic_fun of ct_ID_OPT_NE_LIST * ct_TACTIC_COM
-  | CT_then of ct_TACTIC_COM * ct_TACTIC_COM list
-  | CT_transitivity of ct_FORMULA
-  | CT_trivial
-  | CT_trivial_with of ct_ID_NE_LIST_OR_STAR
-  | CT_truecut of ct_ID_OPT * ct_FORMULA
-  | CT_try of ct_TACTIC_COM
-  | CT_use of ct_FORMULA
-  | CT_use_inversion of ct_ID_OR_INT * ct_FORMULA * ct_ID_LIST
-  | CT_user_tac of ct_ID * ct_TARG_LIST
-and ct_TACTIC_OPT =
-    CT_coerce_NONE_to_TACTIC_OPT of ct_NONE
-  | CT_coerce_TACTIC_COM_to_TACTIC_OPT of ct_TACTIC_COM
-and ct_TAC_DEF =
-    CT_tac_def of ct_ID * ct_TACTIC_COM
-and ct_TAC_DEF_NE_LIST =
-    CT_tac_def_ne_list of ct_TAC_DEF * ct_TAC_DEF list
-and ct_TARG =
-    CT_coerce_BINDING_to_TARG of ct_BINDING
-  | CT_coerce_COFIXTAC_to_TARG of ct_COFIXTAC
-  | CT_coerce_FIXTAC_to_TARG of ct_FIXTAC
-  | CT_coerce_FORMULA_OR_INT_to_TARG of ct_FORMULA_OR_INT
-  | CT_coerce_PATTERN_to_TARG of ct_PATTERN
-  | CT_coerce_SCOMMENT_CONTENT_to_TARG of ct_SCOMMENT_CONTENT
-  | CT_coerce_SIGNED_INT_LIST_to_TARG of ct_SIGNED_INT_LIST
-  | CT_coerce_SINGLE_OPTION_VALUE_to_TARG of ct_SINGLE_OPTION_VALUE
-  | CT_coerce_SPEC_LIST_to_TARG of ct_SPEC_LIST
-  | CT_coerce_TACTIC_COM_to_TARG of ct_TACTIC_COM
-  | CT_coerce_TARG_LIST_to_TARG of ct_TARG_LIST
-  | CT_coerce_UNFOLD_to_TARG of ct_UNFOLD
-  | CT_coerce_UNFOLD_NE_LIST_to_TARG of ct_UNFOLD_NE_LIST
-and ct_TARG_LIST =
-    CT_targ_list of ct_TARG list
-and ct_TERM_CHANGE =
-    CT_check_term of ct_FORMULA
-  | CT_inst_term of ct_ID * ct_FORMULA
-and ct_TEXT =
-    CT_coerce_ID_to_TEXT of ct_ID
-  | CT_text_formula of ct_FORMULA
-  | CT_text_h of ct_TEXT list
-  | CT_text_hv of ct_TEXT list
-  | CT_text_op of ct_TEXT list
-  | CT_text_path of ct_SIGNED_INT_LIST
-  | 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_BINDER_LIST * ct_FORMULA
-and ct_THM =
-    CT_thm of string
-and ct_THM_OPT =
-    CT_coerce_NONE_to_THM_OPT of ct_NONE
-  | CT_coerce_THM_to_THM_OPT of ct_THM
-and ct_TYPED_FORMULA =
-    CT_typed_formula of ct_FORMULA * ct_FORMULA
-and ct_UNFOLD =
-    CT_coerce_ID_to_UNFOLD of ct_ID
-  | CT_unfold_occ of ct_ID * ct_INT_NE_LIST
-and ct_UNFOLD_NE_LIST =
-    CT_unfold_ne_list of ct_UNFOLD * ct_UNFOLD list
-and ct_USING =
-    CT_coerce_NONE_to_USING of ct_NONE
-  | CT_using of ct_FORMULA * ct_SPEC_LIST
-and ct_USINGTDB =
-    CT_coerce_NONE_to_USINGTDB of ct_NONE
-  | CT_usingtdb
-and ct_VAR =
-    CT_var of string
-and ct_VARG =
-    CT_coerce_AST_to_VARG of ct_AST
-  | CT_coerce_AST_LIST_to_VARG of ct_AST_LIST
-  | CT_coerce_BINDER_to_VARG of ct_BINDER
-  | CT_coerce_BINDER_LIST_to_VARG of ct_BINDER_LIST
-  | CT_coerce_BINDER_NE_LIST_to_VARG of ct_BINDER_NE_LIST
-  | CT_coerce_FORMULA_LIST_to_VARG of ct_FORMULA_LIST
-  | CT_coerce_FORMULA_OPT_to_VARG of ct_FORMULA_OPT
-  | CT_coerce_FORMULA_OR_INT_to_VARG of ct_FORMULA_OR_INT
-  | CT_coerce_ID_OPT_OR_ALL_to_VARG of ct_ID_OPT_OR_ALL
-  | CT_coerce_ID_OR_INT_OPT_to_VARG of ct_ID_OR_INT_OPT
-  | CT_coerce_INT_LIST_to_VARG of ct_INT_LIST
-  | CT_coerce_SCOMMENT_CONTENT_to_VARG of ct_SCOMMENT_CONTENT
-  | CT_coerce_STRING_OPT_to_VARG of ct_STRING_OPT
-  | CT_coerce_TACTIC_OPT_to_VARG of ct_TACTIC_OPT
-  | CT_coerce_VARG_LIST_to_VARG of ct_VARG_LIST
-and ct_VARG_LIST =
-    CT_varg_list of ct_VARG list
-and ct_VERBOSE_OPT =
-    CT_coerce_NONE_to_VERBOSE_OPT of ct_NONE
-  | CT_verbose
-;;