aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface/ascent.mli
blob: 335afddd227c33723f0a595652b12c9c25b04421 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
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_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_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_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_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 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_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
;;