diff options
Diffstat (limited to 'contrib/interface/ascent.mli')
| -rw-r--r-- | contrib/interface/ascent.mli | 784 |
1 files changed, 784 insertions, 0 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli new file mode 100644 index 00000000..61d0d5a3 --- /dev/null +++ b/contrib/interface/ascent.mli @@ -0,0 +1,784 @@ +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 ct_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 * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_BINDING_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_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 * 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_opaque of ct_ID_NE_LIST + | 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_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_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_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_transparent of ct_ID_NE_LIST + | 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_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 * ct_FORMULA + | CT_module_type_with_mod of ct_MODULE_TYPE * ct_ID * 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_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_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 * ct_USING * ct_INTRO_PATT_OPT + | CT_new_induction of ct_FORMULA_OR_INT * 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_rewrite_lr of ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT + | CT_rewrite_rl of ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT + | 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 +;; |