← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to contrib/interface/vtp.ml

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
contrib/interface/vtp.ml
 
1
open Ascent;;
 
2
open Pp;;
 
3
 
 
4
(* LEM: This is actually generated automatically *)
 
5
 
 
6
let fNODE s n =
 
7
    (str "n\n") ++
 
8
    (str ("vernac$" ^ s)) ++
 
9
    (str "\n") ++
 
10
    (int n) ++
 
11
    (str "\n");;
 
12
 
 
13
let fATOM s1 =
 
14
    (str "a\n") ++
 
15
    (str ("vernac$" ^ s1)) ++
 
16
    (str "\n");;
 
17
 
 
18
let f_atom_string = str;;
 
19
let f_atom_int = int;;
 
20
let rec fAST = function
 
21
| CT_coerce_ID_OR_INT_to_AST x -> fID_OR_INT x
 
22
| CT_coerce_ID_OR_STRING_to_AST x -> fID_OR_STRING x
 
23
| CT_coerce_SINGLE_OPTION_VALUE_to_AST x -> fSINGLE_OPTION_VALUE x
 
24
| CT_astnode(x1, x2) ->
 
25
   fID x1 ++
 
26
   fAST_LIST x2 ++
 
27
   fNODE "astnode" 2
 
28
| CT_astpath(x1) ->
 
29
   fID_LIST x1 ++
 
30
   fNODE "astpath" 1
 
31
| CT_astslam(x1, x2) ->
 
32
   fID_OPT x1 ++
 
33
   fAST x2 ++
 
34
   fNODE "astslam" 2
 
35
and fAST_LIST = function
 
36
| CT_ast_list l ->
 
37
   (List.fold_left (++) (mt()) (List.map fAST l)) ++
 
38
   fNODE "ast_list" (List.length l)
 
39
and fBINARY = function
 
40
| CT_binary x -> fATOM "binary" ++
 
41
   (f_atom_int x) ++
 
42
   str "\n"
 
43
and fBINDER = function
 
44
| CT_coerce_DEF_to_BINDER x -> fDEF x
 
45
| CT_binder(x1, x2) ->
 
46
   fID_OPT_NE_LIST x1 ++
 
47
   fFORMULA x2 ++
 
48
   fNODE "binder" 2
 
49
| CT_binder_coercion(x1, x2) ->
 
50
   fID_OPT_NE_LIST x1 ++
 
51
   fFORMULA x2 ++
 
52
   fNODE "binder_coercion" 2
 
53
and fBINDER_LIST = function
 
54
| CT_binder_list l ->
 
55
   (List.fold_left (++) (mt()) (List.map fBINDER l)) ++
 
56
   fNODE "binder_list" (List.length l)
 
57
and fBINDER_NE_LIST = function
 
58
| CT_binder_ne_list(x,l) ->
 
59
   fBINDER x ++
 
60
   (List.fold_left (++) (mt()) (List.map fBINDER l)) ++
 
61
   fNODE "binder_ne_list" (1 + (List.length l))
 
62
and fBINDING = function
 
63
| CT_binding(x1, x2) ->
 
64
   fID_OR_INT x1 ++
 
65
   fFORMULA x2 ++
 
66
   fNODE "binding" 2
 
67
and fBINDING_LIST = function
 
68
| CT_binding_list l ->
 
69
   (List.fold_left (++) (mt()) (List.map fBINDING l)) ++
 
70
   fNODE "binding_list" (List.length l)
 
71
and fBOOL = function
 
72
| CT_false -> fNODE "false" 0
 
73
| CT_true -> fNODE "true" 0
 
74
and fCASE = function
 
75
| CT_case x -> fATOM "case" ++
 
76
   (f_atom_string x) ++
 
77
   str "\n"
 
78
and fCLAUSE = function
 
79
| CT_clause(x1, x2) ->
 
80
   fHYP_LOCATION_LIST_OR_STAR x1 ++
 
81
   fSTAR_OPT x2 ++
 
82
   fNODE "clause" 2
 
83
and fCOERCION_OPT = function
 
84
| CT_coerce_NONE_to_COERCION_OPT x -> fNONE x
 
85
| CT_coercion_atm -> fNODE "coercion_atm" 0
 
86
and fCOFIXTAC = function
 
87
| CT_cofixtac(x1, x2) ->
 
88
   fID x1 ++
 
89
   fFORMULA x2 ++
 
90
   fNODE "cofixtac" 2
 
91
and fCOFIX_REC = function
 
92
| CT_cofix_rec(x1, x2, x3, x4) ->
 
93
   fID x1 ++
 
94
   fBINDER_LIST x2 ++
 
95
   fFORMULA x3 ++
 
96
   fFORMULA x4 ++
 
97
   fNODE "cofix_rec" 4
 
98
and fCOFIX_REC_LIST = function
 
99
| CT_cofix_rec_list(x,l) ->
 
100
   fCOFIX_REC x ++
 
101
   (List.fold_left (++) (mt()) (List.map fCOFIX_REC l)) ++
 
102
   fNODE "cofix_rec_list" (1 + (List.length l))
 
103
and fCOFIX_TAC_LIST = function
 
104
| CT_cofix_tac_list l ->
 
105
   (List.fold_left (++) (mt()) (List.map fCOFIXTAC l)) ++
 
106
   fNODE "cofix_tac_list" (List.length l)
 
107
and fCOMMAND = function
 
108
| CT_coerce_COMMAND_LIST_to_COMMAND x -> fCOMMAND_LIST x
 
109
| CT_coerce_EVAL_CMD_to_COMMAND x -> fEVAL_CMD x
 
110
| CT_coerce_SECTION_BEGIN_to_COMMAND x -> fSECTION_BEGIN x
 
111
| CT_coerce_THEOREM_GOAL_to_COMMAND x -> fTHEOREM_GOAL x
 
112
| CT_abort(x1) ->
 
113
   fID_OPT_OR_ALL x1 ++
 
114
   fNODE "abort" 1
 
115
| CT_abstraction(x1, x2, x3) ->
 
116
   fID x1 ++
 
117
   fFORMULA x2 ++
 
118
   fINT_LIST x3 ++
 
119
   fNODE "abstraction" 3
 
120
| CT_add_field(x1, x2, x3, x4) ->
 
121
   fFORMULA x1 ++
 
122
   fFORMULA x2 ++
 
123
   fFORMULA x3 ++
 
124
   fFORMULA_OPT x4 ++
 
125
   fNODE "add_field" 4
 
126
| CT_add_natural_feature(x1, x2) ->
 
127
   fNATURAL_FEATURE x1 ++
 
128
   fID x2 ++
 
129
   fNODE "add_natural_feature" 2
 
130
| CT_addpath(x1, x2) ->
 
131
   fSTRING x1 ++
 
132
   fID_OPT x2 ++
 
133
   fNODE "addpath" 2
 
134
| CT_arguments_scope(x1, x2) ->
 
135
   fID x1 ++
 
136
   fID_OPT_LIST x2 ++
 
137
   fNODE "arguments_scope" 2
 
138
| CT_bind_scope(x1, x2) ->
 
139
   fID x1 ++
 
140
   fID_NE_LIST x2 ++
 
141
   fNODE "bind_scope" 2
 
142
| CT_cd(x1) ->
 
143
   fSTRING_OPT x1 ++
 
144
   fNODE "cd" 1
 
145
| CT_check(x1) ->
 
146
   fFORMULA x1 ++
 
147
   fNODE "check" 1
 
148
| CT_class(x1) ->
 
149
   fID x1 ++
 
150
   fNODE "class" 1
 
151
| CT_close_scope(x1) ->
 
152
   fID x1 ++
 
153
   fNODE "close_scope" 1
 
154
| CT_coercion(x1, x2, x3, x4, x5) ->
 
155
   fLOCAL_OPT x1 ++
 
156
   fIDENTITY_OPT x2 ++
 
157
   fID x3 ++
 
158
   fID x4 ++
 
159
   fID x5 ++
 
160
   fNODE "coercion" 5
 
161
| CT_cofix_decl(x1) ->
 
162
   fCOFIX_REC_LIST x1 ++
 
163
   fNODE "cofix_decl" 1
 
164
| CT_compile_module(x1, x2, x3) ->
 
165
   fVERBOSE_OPT x1 ++
 
166
   fID x2 ++
 
167
   fSTRING_OPT x3 ++
 
168
   fNODE "compile_module" 3
 
169
| CT_declare_module(x1, x2, x3, x4) ->
 
170
   fID x1 ++
 
171
   fMODULE_BINDER_LIST x2 ++
 
172
   fMODULE_TYPE_CHECK x3 ++
 
173
   fMODULE_EXPR x4 ++
 
174
   fNODE "declare_module" 4
 
175
| CT_define_notation(x1, x2, x3, x4) ->
 
176
   fSTRING x1 ++
 
177
   fFORMULA x2 ++
 
178
   fMODIFIER_LIST x3 ++
 
179
   fID_OPT x4 ++
 
180
   fNODE "define_notation" 4
 
181
| CT_definition(x1, x2, x3, x4, x5) ->
 
182
   fDEFN x1 ++
 
183
   fID x2 ++
 
184
   fBINDER_LIST x3 ++
 
185
   fDEF_BODY x4 ++
 
186
   fFORMULA_OPT x5 ++
 
187
   fNODE "definition" 5
 
188
| CT_delim_scope(x1, x2) ->
 
189
   fID x1 ++
 
190
   fID x2 ++
 
191
   fNODE "delim_scope" 2
 
192
| CT_delpath(x1) ->
 
193
   fSTRING x1 ++
 
194
   fNODE "delpath" 1
 
195
| CT_derive_depinversion(x1, x2, x3, x4) ->
 
196
   fINV_TYPE x1 ++
 
197
   fID x2 ++
 
198
   fFORMULA x3 ++
 
199
   fSORT_TYPE x4 ++
 
200
   fNODE "derive_depinversion" 4
 
201
| CT_derive_inversion(x1, x2, x3, x4) ->
 
202
   fINV_TYPE x1 ++
 
203
   fINT_OPT x2 ++
 
204
   fID x3 ++
 
205
   fID x4 ++
 
206
   fNODE "derive_inversion" 4
 
207
| CT_derive_inversion_with(x1, x2, x3, x4) ->
 
208
   fINV_TYPE x1 ++
 
209
   fID x2 ++
 
210
   fFORMULA x3 ++
 
211
   fSORT_TYPE x4 ++
 
212
   fNODE "derive_inversion_with" 4
 
213
| CT_explain_proof(x1) ->
 
214
   fINT_LIST x1 ++
 
215
   fNODE "explain_proof" 1
 
216
| CT_explain_prooftree(x1) ->
 
217
   fINT_LIST x1 ++
 
218
   fNODE "explain_prooftree" 1
 
219
| CT_export_id(x1) ->
 
220
   fID_NE_LIST x1 ++
 
221
   fNODE "export_id" 1
 
222
| CT_extract_to_file(x1, x2) ->
 
223
   fSTRING x1 ++
 
224
   fID_NE_LIST x2 ++
 
225
   fNODE "extract_to_file" 2
 
226
| CT_extraction(x1) ->
 
227
   fID_OPT x1 ++
 
228
   fNODE "extraction" 1
 
229
| CT_fix_decl(x1) ->
 
230
   fFIX_REC_LIST x1 ++
 
231
   fNODE "fix_decl" 1
 
232
| CT_focus(x1) ->
 
233
   fINT_OPT x1 ++
 
234
   fNODE "focus" 1
 
235
| CT_go(x1) ->
 
236
   fINT_OR_LOCN x1 ++
 
237
   fNODE "go" 1
 
238
| CT_guarded -> fNODE "guarded" 0
 
239
| CT_hint_destruct(x1, x2, x3, x4, x5, x6) ->
 
240
   fID x1 ++
 
241
   fINT x2 ++
 
242
   fDESTRUCT_LOCATION x3 ++
 
243
   fFORMULA x4 ++
 
244
   fTACTIC_COM x5 ++
 
245
   fID_LIST x6 ++
 
246
   fNODE "hint_destruct" 6
 
247
| CT_hint_extern(x1, x2, x3, x4) ->
 
248
   fINT x1 ++
 
249
   fFORMULA_OPT x2 ++
 
250
   fTACTIC_COM x3 ++
 
251
   fID_LIST x4 ++
 
252
   fNODE "hint_extern" 4
 
253
| CT_hintrewrite(x1, x2, x3, x4) ->
 
254
   fORIENTATION x1 ++
 
255
   fFORMULA_NE_LIST x2 ++
 
256
   fID x3 ++
 
257
   fTACTIC_COM x4 ++
 
258
   fNODE "hintrewrite" 4
 
259
| CT_hints(x1, x2, x3) ->
 
260
   fID x1 ++
 
261
   fID_NE_LIST x2 ++
 
262
   fID_LIST x3 ++
 
263
   fNODE "hints" 3
 
264
| CT_hints_immediate(x1, x2) ->
 
265
   fFORMULA_NE_LIST x1 ++
 
266
   fID_LIST x2 ++
 
267
   fNODE "hints_immediate" 2
 
268
| CT_hints_resolve(x1, x2) ->
 
269
   fFORMULA_NE_LIST x1 ++
 
270
   fID_LIST x2 ++
 
271
   fNODE "hints_resolve" 2
 
272
| CT_hyp_search_pattern(x1, x2) ->
 
273
   fFORMULA x1 ++
 
274
   fIN_OR_OUT_MODULES x2 ++
 
275
   fNODE "hyp_search_pattern" 2
 
276
| CT_implicits(x1, x2) ->
 
277
   fID x1 ++
 
278
   fID_LIST_OPT x2 ++
 
279
   fNODE "implicits" 2
 
280
| CT_import_id(x1) ->
 
281
   fID_NE_LIST x1 ++
 
282
   fNODE "import_id" 1
 
283
| CT_ind_scheme(x1) ->
 
284
   fSCHEME_SPEC_LIST x1 ++
 
285
   fNODE "ind_scheme" 1
 
286
| CT_infix(x1, x2, x3, x4) ->
 
287
   fSTRING x1 ++
 
288
   fID x2 ++
 
289
   fMODIFIER_LIST x3 ++
 
290
   fID_OPT x4 ++
 
291
   fNODE "infix" 4
 
292
| CT_inline(x1) ->
 
293
   fID_NE_LIST x1 ++
 
294
   fNODE "inline" 1
 
295
| CT_inspect(x1) ->
 
296
   fINT x1 ++
 
297
   fNODE "inspect" 1
 
298
| CT_kill_node(x1) ->
 
299
   fINT x1 ++
 
300
   fNODE "kill_node" 1
 
301
| CT_load(x1, x2) ->
 
302
   fVERBOSE_OPT x1 ++
 
303
   fID_OR_STRING x2 ++
 
304
   fNODE "load" 2
 
305
| CT_local_close_scope(x1) ->
 
306
   fID x1 ++
 
307
   fNODE "local_close_scope" 1
 
308
| CT_local_define_notation(x1, x2, x3, x4) ->
 
309
   fSTRING x1 ++
 
310
   fFORMULA x2 ++
 
311
   fMODIFIER_LIST x3 ++
 
312
   fID_OPT x4 ++
 
313
   fNODE "local_define_notation" 4
 
314
| CT_local_hint_destruct(x1, x2, x3, x4, x5, x6) ->
 
315
   fID x1 ++
 
316
   fINT x2 ++
 
317
   fDESTRUCT_LOCATION x3 ++
 
318
   fFORMULA x4 ++
 
319
   fTACTIC_COM x5 ++
 
320
   fID_LIST x6 ++
 
321
   fNODE "local_hint_destruct" 6
 
322
| CT_local_hint_extern(x1, x2, x3, x4) ->
 
323
   fINT x1 ++
 
324
   fFORMULA x2 ++
 
325
   fTACTIC_COM x3 ++
 
326
   fID_LIST x4 ++
 
327
   fNODE "local_hint_extern" 4
 
328
| CT_local_hints(x1, x2, x3) ->
 
329
   fID x1 ++
 
330
   fID_NE_LIST x2 ++
 
331
   fID_LIST x3 ++
 
332
   fNODE "local_hints" 3
 
333
| CT_local_hints_immediate(x1, x2) ->
 
334
   fFORMULA_NE_LIST x1 ++
 
335
   fID_LIST x2 ++
 
336
   fNODE "local_hints_immediate" 2
 
337
| CT_local_hints_resolve(x1, x2) ->
 
338
   fFORMULA_NE_LIST x1 ++
 
339
   fID_LIST x2 ++
 
340
   fNODE "local_hints_resolve" 2
 
341
| CT_local_infix(x1, x2, x3, x4) ->
 
342
   fSTRING x1 ++
 
343
   fID x2 ++
 
344
   fMODIFIER_LIST x3 ++
 
345
   fID_OPT x4 ++
 
346
   fNODE "local_infix" 4
 
347
| CT_local_open_scope(x1) ->
 
348
   fID x1 ++
 
349
   fNODE "local_open_scope" 1
 
350
| CT_local_reserve_notation(x1, x2) ->
 
351
   fSTRING x1 ++
 
352
   fMODIFIER_LIST x2 ++
 
353
   fNODE "local_reserve_notation" 2
 
354
| CT_locate(x1) ->
 
355
   fID x1 ++
 
356
   fNODE "locate" 1
 
357
| CT_locate_file(x1) ->
 
358
   fSTRING x1 ++
 
359
   fNODE "locate_file" 1
 
360
| CT_locate_lib(x1) ->
 
361
   fID x1 ++
 
362
   fNODE "locate_lib" 1
 
363
| CT_locate_notation(x1) ->
 
364
   fSTRING x1 ++
 
365
   fNODE "locate_notation" 1
 
366
| CT_mind_decl(x1, x2) ->
 
367
   fCO_IND x1 ++
 
368
   fIND_SPEC_LIST x2 ++
 
369
   fNODE "mind_decl" 2
 
370
| CT_ml_add_path(x1) ->
 
371
   fSTRING x1 ++
 
372
   fNODE "ml_add_path" 1
 
373
| CT_ml_declare_modules(x1) ->
 
374
   fSTRING_NE_LIST x1 ++
 
375
   fNODE "ml_declare_modules" 1
 
376
| CT_ml_print_modules -> fNODE "ml_print_modules" 0
 
377
| CT_ml_print_path -> fNODE "ml_print_path" 0
 
378
| CT_module(x1, x2, x3, x4) ->
 
379
   fID x1 ++
 
380
   fMODULE_BINDER_LIST x2 ++
 
381
   fMODULE_TYPE_CHECK x3 ++
 
382
   fMODULE_EXPR x4 ++
 
383
   fNODE "module" 4
 
384
| CT_module_type_decl(x1, x2, x3) ->
 
385
   fID x1 ++
 
386
   fMODULE_BINDER_LIST x2 ++
 
387
   fMODULE_TYPE_OPT x3 ++
 
388
   fNODE "module_type_decl" 3
 
389
| CT_no_inline(x1) ->
 
390
   fID_NE_LIST x1 ++
 
391
   fNODE "no_inline" 1
 
392
| CT_omega_flag(x1, x2) ->
 
393
   fOMEGA_MODE x1 ++
 
394
   fOMEGA_FEATURE x2 ++
 
395
   fNODE "omega_flag" 2
 
396
| CT_open_scope(x1) ->
 
397
   fID x1 ++
 
398
   fNODE "open_scope" 1
 
399
| CT_print -> fNODE "print" 0
 
400
| CT_print_about(x1) ->
 
401
   fID x1 ++
 
402
   fNODE "print_about" 1
 
403
| CT_print_all -> fNODE "print_all" 0
 
404
| CT_print_classes -> fNODE "print_classes" 0
 
405
| CT_print_ltac id ->
 
406
   fID id ++
 
407
   fNODE "print_ltac" 1
 
408
| CT_print_coercions -> fNODE "print_coercions" 0
 
409
| CT_print_grammar(x1) ->
 
410
   fGRAMMAR x1 ++
 
411
   fNODE "print_grammar" 1
 
412
| CT_print_graph -> fNODE "print_graph" 0
 
413
| CT_print_hint(x1) ->
 
414
   fID_OPT x1 ++
 
415
   fNODE "print_hint" 1
 
416
| CT_print_hintdb(x1) ->
 
417
   fID_OR_STAR x1 ++
 
418
   fNODE "print_hintdb" 1
 
419
| CT_print_rewrite_hintdb(x1) ->
 
420
   fID x1 ++
 
421
   fNODE "print_rewrite_hintdb" 1
 
422
| CT_print_id(x1) ->
 
423
   fID x1 ++
 
424
   fNODE "print_id" 1
 
425
| CT_print_implicit(x1) ->
 
426
   fID x1 ++
 
427
   fNODE "print_implicit" 1
 
428
| CT_print_loadpath -> fNODE "print_loadpath" 0
 
429
| CT_print_module(x1) ->
 
430
   fID x1 ++
 
431
   fNODE "print_module" 1
 
432
| CT_print_module_type(x1) ->
 
433
   fID x1 ++
 
434
   fNODE "print_module_type" 1
 
435
| CT_print_modules -> fNODE "print_modules" 0
 
436
| CT_print_natural(x1) ->
 
437
   fID x1 ++
 
438
   fNODE "print_natural" 1
 
439
| CT_print_natural_feature(x1) ->
 
440
   fNATURAL_FEATURE x1 ++
 
441
   fNODE "print_natural_feature" 1
 
442
| CT_print_opaqueid(x1) ->
 
443
   fID x1 ++
 
444
   fNODE "print_opaqueid" 1
 
445
| CT_print_path(x1, x2) ->
 
446
   fID x1 ++
 
447
   fID x2 ++
 
448
   fNODE "print_path" 2
 
449
| CT_print_proof(x1) ->
 
450
   fID x1 ++
 
451
   fNODE "print_proof" 1
 
452
| CT_print_scope(x1) ->
 
453
   fID x1 ++
 
454
   fNODE "print_scope" 1
 
455
| CT_print_setoids -> fNODE "print_setoids" 0
 
456
| CT_print_scopes -> fNODE "print_scopes" 0
 
457
| CT_print_section(x1) ->
 
458
   fID x1 ++
 
459
   fNODE "print_section" 1
 
460
| CT_print_states -> fNODE "print_states" 0
 
461
| CT_print_tables -> fNODE "print_tables" 0
 
462
| CT_print_universes(x1) ->
 
463
   fSTRING_OPT x1 ++
 
464
   fNODE "print_universes" 1
 
465
| CT_print_visibility(x1) ->
 
466
   fID_OPT x1 ++
 
467
   fNODE "print_visibility" 1
 
468
| CT_proof(x1) ->
 
469
   fFORMULA x1 ++
 
470
   fNODE "proof" 1
 
471
| CT_proof_no_op -> fNODE "proof_no_op" 0
 
472
| CT_proof_with(x1) ->
 
473
   fTACTIC_COM x1 ++
 
474
   fNODE "proof_with" 1
 
475
| CT_pwd -> fNODE "pwd" 0
 
476
| CT_quit -> fNODE "quit" 0
 
477
| CT_read_module(x1) ->
 
478
   fID x1 ++
 
479
   fNODE "read_module" 1
 
480
| CT_rec_ml_add_path(x1) ->
 
481
   fSTRING x1 ++
 
482
   fNODE "rec_ml_add_path" 1
 
483
| CT_recaddpath(x1, x2) ->
 
484
   fSTRING x1 ++
 
485
   fID_OPT x2 ++
 
486
   fNODE "recaddpath" 2
 
487
| CT_record(x1, x2, x3, x4, x5, x6) ->
 
488
   fCOERCION_OPT x1 ++
 
489
   fID x2 ++
 
490
   fBINDER_LIST x3 ++
 
491
   fFORMULA x4 ++
 
492
   fID_OPT x5 ++
 
493
   fRECCONSTR_LIST x6 ++
 
494
   fNODE "record" 6
 
495
| CT_remove_natural_feature(x1, x2) ->
 
496
   fNATURAL_FEATURE x1 ++
 
497
   fID x2 ++
 
498
   fNODE "remove_natural_feature" 2
 
499
| CT_require(x1, x2, x3) ->
 
500
   fIMPEXP x1 ++
 
501
   fSPEC_OPT x2 ++
 
502
   fID_NE_LIST_OR_STRING x3 ++
 
503
   fNODE "require" 3
 
504
| CT_reserve(x1, x2) ->
 
505
   fID_NE_LIST x1 ++
 
506
   fFORMULA x2 ++
 
507
   fNODE "reserve" 2
 
508
| CT_reserve_notation(x1, x2) ->
 
509
   fSTRING x1 ++
 
510
   fMODIFIER_LIST x2 ++
 
511
   fNODE "reserve_notation" 2
 
512
| CT_reset(x1) ->
 
513
   fID x1 ++
 
514
   fNODE "reset" 1
 
515
| CT_reset_section(x1) ->
 
516
   fID x1 ++
 
517
   fNODE "reset_section" 1
 
518
| CT_restart -> fNODE "restart" 0
 
519
| CT_restore_state(x1) ->
 
520
   fID x1 ++
 
521
   fNODE "restore_state" 1
 
522
| CT_resume(x1) ->
 
523
   fID_OPT x1 ++
 
524
   fNODE "resume" 1
 
525
| CT_save(x1, x2) ->
 
526
   fTHM_OPT x1 ++
 
527
   fID_OPT x2 ++
 
528
   fNODE "save" 2
 
529
| CT_scomments(x1) ->
 
530
   fSCOMMENT_CONTENT_LIST x1 ++
 
531
   fNODE "scomments" 1
 
532
| CT_search(x1, x2) ->
 
533
   fID x1 ++
 
534
   fIN_OR_OUT_MODULES x2 ++
 
535
   fNODE "search" 2
 
536
| CT_search_about(x1, x2) ->
 
537
   fID_OR_STRING_NE_LIST x1 ++
 
538
   fIN_OR_OUT_MODULES x2 ++
 
539
   fNODE "search_about" 2
 
540
| CT_search_pattern(x1, x2) ->
 
541
   fFORMULA x1 ++
 
542
   fIN_OR_OUT_MODULES x2 ++
 
543
   fNODE "search_pattern" 2
 
544
| CT_search_rewrite(x1, x2) ->
 
545
   fFORMULA x1 ++
 
546
   fIN_OR_OUT_MODULES x2 ++
 
547
   fNODE "search_rewrite" 2
 
548
| CT_section_end(x1) ->
 
549
   fID x1 ++
 
550
   fNODE "section_end" 1
 
551
| CT_section_struct(x1, x2, x3) ->
 
552
   fSECTION_BEGIN x1 ++
 
553
   fSECTION_BODY x2 ++
 
554
   fCOMMAND x3 ++
 
555
   fNODE "section_struct" 3
 
556
| CT_set_natural(x1) ->
 
557
   fID x1 ++
 
558
   fNODE "set_natural" 1
 
559
| CT_set_natural_default -> fNODE "set_natural_default" 0
 
560
| CT_set_option(x1) ->
 
561
   fTABLE x1 ++
 
562
   fNODE "set_option" 1
 
563
| CT_set_option_value(x1, x2) ->
 
564
   fTABLE x1 ++
 
565
   fSINGLE_OPTION_VALUE x2 ++
 
566
   fNODE "set_option_value" 2
 
567
| CT_set_option_value2(x1, x2) ->
 
568
   fTABLE x1 ++
 
569
   fID_OR_STRING_NE_LIST x2 ++
 
570
   fNODE "set_option_value2" 2
 
571
| CT_sethyp(x1) ->
 
572
   fINT x1 ++
 
573
   fNODE "sethyp" 1
 
574
| CT_setundo(x1) ->
 
575
   fINT x1 ++
 
576
   fNODE "setundo" 1
 
577
| CT_show_existentials -> fNODE "show_existentials" 0
 
578
| CT_show_goal(x1) ->
 
579
   fINT_OPT x1 ++
 
580
   fNODE "show_goal" 1
 
581
| CT_show_implicit(x1) ->
 
582
   fINT x1 ++
 
583
   fNODE "show_implicit" 1
 
584
| CT_show_intro -> fNODE "show_intro" 0
 
585
| CT_show_intros -> fNODE "show_intros" 0
 
586
| CT_show_node -> fNODE "show_node" 0
 
587
| CT_show_proof -> fNODE "show_proof" 0
 
588
| CT_show_proofs -> fNODE "show_proofs" 0
 
589
| CT_show_script -> fNODE "show_script" 0
 
590
| CT_show_tree -> fNODE "show_tree" 0
 
591
| CT_solve(x1, x2, x3) ->
 
592
   fINT x1 ++
 
593
   fTACTIC_COM x2 ++
 
594
   fDOTDOT_OPT x3 ++
 
595
   fNODE "solve" 3
 
596
| CT_strategy(CT_level_list x1) ->
 
597
   List.fold_left (++) (mt())
 
598
     (List.map (fun(l,q) -> fLEVEL l ++ fID_LIST q ++ fNODE "pair"2) x1) ++
 
599
   fNODE "strategy" (List.length x1)
 
600
| CT_suspend -> fNODE "suspend" 0
 
601
| CT_syntax_macro(x1, x2, x3) ->
 
602
   fID x1 ++
 
603
   fFORMULA x2 ++
 
604
   fINT_OPT x3 ++
 
605
   fNODE "syntax_macro" 3
 
606
| CT_tactic_definition(x1) ->
 
607
   fTAC_DEF_NE_LIST x1 ++
 
608
   fNODE "tactic_definition" 1
 
609
| CT_test_natural_feature(x1, x2) ->
 
610
   fNATURAL_FEATURE x1 ++
 
611
   fID x2 ++
 
612
   fNODE "test_natural_feature" 2
 
613
| CT_theorem_struct(x1, x2) ->
 
614
   fTHEOREM_GOAL x1 ++
 
615
   fPROOF_SCRIPT x2 ++
 
616
   fNODE "theorem_struct" 2
 
617
| CT_time(x1) ->
 
618
   fCOMMAND x1 ++
 
619
   fNODE "time" 1
 
620
| CT_undo(x1) ->
 
621
   fINT_OPT x1 ++
 
622
   fNODE "undo" 1
 
623
| CT_unfocus -> fNODE "unfocus" 0
 
624
| CT_unset_option(x1) ->
 
625
   fTABLE x1 ++
 
626
   fNODE "unset_option" 1
 
627
| CT_unsethyp -> fNODE "unsethyp" 0
 
628
| CT_unsetundo -> fNODE "unsetundo" 0
 
629
| CT_user_vernac(x1, x2) ->
 
630
   fID x1 ++
 
631
   fVARG_LIST x2 ++
 
632
   fNODE "user_vernac" 2
 
633
| CT_variable(x1, x2) ->
 
634
   fVAR x1 ++
 
635
   fBINDER_NE_LIST x2 ++
 
636
   fNODE "variable" 2
 
637
| CT_write_module(x1, x2) ->
 
638
   fID x1 ++
 
639
   fSTRING_OPT x2 ++
 
640
   fNODE "write_module" 2
 
641
and fLEVEL = function
 
642
| CT_Opaque -> fNODE "opaque" 0
 
643
| CT_Level n -> fINT n ++ fNODE "level" 1
 
644
| CT_Expand -> fNODE "expand" 0
 
645
and fCOMMAND_LIST = function
 
646
| CT_command_list(x,l) ->
 
647
   fCOMMAND x ++
 
648
   (List.fold_left (++) (mt()) (List.map fCOMMAND l)) ++
 
649
   fNODE "command_list" (1 + (List.length l))
 
650
and fCOMMENT = function
 
651
| CT_comment x -> fATOM "comment" ++
 
652
   (f_atom_string x) ++
 
653
   str "\n"
 
654
and fCOMMENT_S = function
 
655
| CT_comment_s l ->
 
656
   (List.fold_left (++) (mt()) (List.map fCOMMENT l)) ++
 
657
   fNODE "comment_s" (List.length l)
 
658
and fCONSTR = function
 
659
| CT_constr(x1, x2) ->
 
660
   fID x1 ++
 
661
   fFORMULA x2 ++
 
662
   fNODE "constr" 2
 
663
| CT_constr_coercion(x1, x2) ->
 
664
   fID x1 ++
 
665
   fFORMULA x2 ++
 
666
   fNODE "constr_coercion" 2
 
667
and fCONSTR_LIST = function
 
668
| CT_constr_list l ->
 
669
   (List.fold_left (++) (mt()) (List.map fCONSTR l)) ++
 
670
   fNODE "constr_list" (List.length l)
 
671
and fCONTEXT_HYP_LIST = function
 
672
| CT_context_hyp_list l ->
 
673
   (List.fold_left (++) (mt()) (List.map fPREMISE_PATTERN l)) ++
 
674
   fNODE "context_hyp_list" (List.length l)
 
675
and fCONTEXT_PATTERN = function
 
676
| CT_coerce_FORMULA_to_CONTEXT_PATTERN x -> fFORMULA x
 
677
| CT_context(x1, x2) ->
 
678
   fID_OPT x1 ++
 
679
   fFORMULA x2 ++
 
680
   fNODE "context" 2
 
681
and fCONTEXT_RULE = function
 
682
| CT_context_rule(x1, x2, x3) ->
 
683
   fCONTEXT_HYP_LIST x1 ++
 
684
   fCONTEXT_PATTERN x2 ++
 
685
   fTACTIC_COM x3 ++
 
686
   fNODE "context_rule" 3
 
687
| CT_def_context_rule(x1) ->
 
688
   fTACTIC_COM x1 ++
 
689
   fNODE "def_context_rule" 1
 
690
and fCONVERSION_FLAG = function
 
691
| CT_beta -> fNODE "beta" 0
 
692
| CT_delta -> fNODE "delta" 0
 
693
| CT_evar -> fNODE "evar" 0
 
694
| CT_iota -> fNODE "iota" 0
 
695
| CT_zeta -> fNODE "zeta" 0
 
696
and fCONVERSION_FLAG_LIST = function
 
697
| CT_conversion_flag_list l ->
 
698
   (List.fold_left (++) (mt()) (List.map fCONVERSION_FLAG l)) ++
 
699
   fNODE "conversion_flag_list" (List.length l)
 
700
and fCONV_SET = function
 
701
| CT_unf l ->
 
702
   (List.fold_left (++) (mt()) (List.map fID l)) ++
 
703
   fNODE "unf" (List.length l)
 
704
| CT_unfbut l ->
 
705
   (List.fold_left (++) (mt()) (List.map fID l)) ++
 
706
   fNODE "unfbut" (List.length l)
 
707
and fCO_IND = function
 
708
| CT_co_ind x -> fATOM "co_ind" ++
 
709
   (f_atom_string x) ++
 
710
   str "\n"
 
711
and fDECL_NOTATION_OPT = function
 
712
| CT_coerce_NONE_to_DECL_NOTATION_OPT x -> fNONE x
 
713
| CT_decl_notation(x1, x2, x3) ->
 
714
   fSTRING x1 ++
 
715
   fFORMULA x2 ++
 
716
   fID_OPT x3 ++
 
717
   fNODE "decl_notation" 3
 
718
and fDEF = function
 
719
| CT_def(x1, x2) ->
 
720
   fID_OPT x1 ++
 
721
   fFORMULA x2 ++
 
722
   fNODE "def" 2
 
723
and fDEFN = function
 
724
| CT_defn x -> fATOM "defn" ++
 
725
   (f_atom_string x) ++
 
726
   str "\n"
 
727
and fDEFN_OR_THM = function
 
728
| CT_coerce_DEFN_to_DEFN_OR_THM x -> fDEFN x
 
729
| CT_coerce_THM_to_DEFN_OR_THM x -> fTHM x
 
730
and fDEF_BODY = function
 
731
| CT_coerce_CONTEXT_PATTERN_to_DEF_BODY x -> fCONTEXT_PATTERN x
 
732
| CT_coerce_EVAL_CMD_to_DEF_BODY x -> fEVAL_CMD x
 
733
| CT_type_of(x1) ->
 
734
   fFORMULA x1 ++
 
735
   fNODE "type_of" 1
 
736
and fDEF_BODY_OPT = function
 
737
| CT_coerce_DEF_BODY_to_DEF_BODY_OPT x -> fDEF_BODY x
 
738
| CT_coerce_FORMULA_OPT_to_DEF_BODY_OPT x -> fFORMULA_OPT x
 
739
and fDEP = function
 
740
| CT_dep x -> fATOM "dep" ++
 
741
   (f_atom_string x) ++
 
742
   str "\n"
 
743
and fDESTRUCTING = function
 
744
| CT_coerce_NONE_to_DESTRUCTING x -> fNONE x
 
745
| CT_destructing -> fNODE "destructing" 0
 
746
and fDESTRUCT_LOCATION = function
 
747
| CT_conclusion_location -> fNODE "conclusion_location" 0
 
748
| CT_discardable_hypothesis -> fNODE "discardable_hypothesis" 0
 
749
| CT_hypothesis_location -> fNODE "hypothesis_location" 0
 
750
and fDOTDOT_OPT = function
 
751
| CT_coerce_NONE_to_DOTDOT_OPT x -> fNONE x
 
752
| CT_dotdot -> fNODE "dotdot" 0
 
753
and fEQN = function
 
754
| CT_eqn(x1, x2) ->
 
755
   fMATCH_PATTERN_NE_LIST x1 ++
 
756
   fFORMULA x2 ++
 
757
   fNODE "eqn" 2
 
758
and fEQN_LIST = function
 
759
| CT_eqn_list l ->
 
760
   (List.fold_left (++) (mt()) (List.map fEQN l)) ++
 
761
   fNODE "eqn_list" (List.length l)
 
762
and fEVAL_CMD = function
 
763
| CT_eval(x1, x2, x3) ->
 
764
   fINT_OPT x1 ++
 
765
   fRED_COM x2 ++
 
766
   fFORMULA x3 ++
 
767
   fNODE "eval" 3
 
768
and fFIXTAC = function
 
769
| CT_fixtac(x1, x2, x3) ->
 
770
   fID x1 ++
 
771
   fINT x2 ++
 
772
   fFORMULA x3 ++
 
773
   fNODE "fixtac" 3
 
774
and fFIX_BINDER = function
 
775
| CT_coerce_FIX_REC_to_FIX_BINDER x -> fFIX_REC x
 
776
| CT_fix_binder(x1, x2, x3, x4) ->
 
777
   fID x1 ++
 
778
   fINT x2 ++
 
779
   fFORMULA x3 ++
 
780
   fFORMULA x4 ++
 
781
   fNODE "fix_binder" 4
 
782
and fFIX_BINDER_LIST = function
 
783
| CT_fix_binder_list(x,l) ->
 
784
   fFIX_BINDER x ++
 
785
   (List.fold_left (++) (mt()) (List.map fFIX_BINDER l)) ++
 
786
   fNODE "fix_binder_list" (1 + (List.length l))
 
787
and fFIX_REC = function
 
788
| CT_fix_rec(x1, x2, x3, x4, x5) ->
 
789
   fID x1 ++
 
790
   fBINDER_NE_LIST x2 ++
 
791
   fID_OPT x3 ++
 
792
   fFORMULA x4 ++
 
793
   fFORMULA x5 ++
 
794
   fNODE "fix_rec" 5
 
795
and fFIX_REC_LIST = function
 
796
| CT_fix_rec_list(x,l) ->
 
797
   fFIX_REC x ++
 
798
   (List.fold_left (++) (mt()) (List.map fFIX_REC l)) ++
 
799
   fNODE "fix_rec_list" (1 + (List.length l))
 
800
and fFIX_TAC_LIST = function
 
801
| CT_fix_tac_list l ->
 
802
   (List.fold_left (++) (mt()) (List.map fFIXTAC l)) ++
 
803
   fNODE "fix_tac_list" (List.length l)
 
804
and fFORMULA = function
 
805
| CT_coerce_BINARY_to_FORMULA x -> fBINARY x
 
806
| CT_coerce_ID_to_FORMULA x -> fID x
 
807
| CT_coerce_NUM_to_FORMULA x -> fNUM x
 
808
| CT_coerce_SORT_TYPE_to_FORMULA x -> fSORT_TYPE x
 
809
| CT_coerce_TYPED_FORMULA_to_FORMULA x -> fTYPED_FORMULA x
 
810
| CT_appc(x1, x2) ->
 
811
   fFORMULA x1 ++
 
812
   fFORMULA_NE_LIST x2 ++
 
813
   fNODE "appc" 2
 
814
| CT_arrowc(x1, x2) ->
 
815
   fFORMULA x1 ++
 
816
   fFORMULA x2 ++
 
817
   fNODE "arrowc" 2
 
818
| CT_bang(x1) ->
 
819
   fFORMULA x1 ++
 
820
   fNODE "bang" 1
 
821
| CT_cases(x1, x2, x3) ->
 
822
   fMATCHED_FORMULA_NE_LIST x1 ++
 
823
   fFORMULA_OPT x2 ++
 
824
   fEQN_LIST x3 ++
 
825
   fNODE "cases" 3
 
826
| CT_cofixc(x1, x2) ->
 
827
   fID x1 ++
 
828
   fCOFIX_REC_LIST x2 ++
 
829
   fNODE "cofixc" 2
 
830
| CT_elimc(x1, x2, x3, x4) ->
 
831
   fCASE x1 ++
 
832
   fFORMULA_OPT x2 ++
 
833
   fFORMULA x3 ++
 
834
   fFORMULA_LIST x4 ++
 
835
   fNODE "elimc" 4
 
836
| CT_existvarc -> fNODE "existvarc" 0
 
837
| CT_fixc(x1, x2) ->
 
838
   fID x1 ++
 
839
   fFIX_BINDER_LIST x2 ++
 
840
   fNODE "fixc" 2
 
841
| CT_if(x1, x2, x3, x4) ->
 
842
   fFORMULA x1 ++
 
843
   fRETURN_INFO x2 ++
 
844
   fFORMULA x3 ++
 
845
   fFORMULA x4 ++
 
846
   fNODE "if" 4
 
847
| CT_inductive_let(x1, x2, x3, x4) ->
 
848
   fFORMULA_OPT x1 ++
 
849
   fID_OPT_NE_LIST x2 ++
 
850
   fFORMULA x3 ++
 
851
   fFORMULA x4 ++
 
852
   fNODE "inductive_let" 4
 
853
| CT_labelled_arg(x1, x2) ->
 
854
   fID x1 ++
 
855
   fFORMULA x2 ++
 
856
   fNODE "labelled_arg" 2
 
857
| CT_lambdac(x1, x2) ->
 
858
   fBINDER_NE_LIST x1 ++
 
859
   fFORMULA x2 ++
 
860
   fNODE "lambdac" 2
 
861
| CT_let_tuple(x1, x2, x3, x4) ->
 
862
   fID_OPT_NE_LIST x1 ++
 
863
   fRETURN_INFO x2 ++
 
864
   fFORMULA x3 ++
 
865
   fFORMULA x4 ++
 
866
   fNODE "let_tuple" 4
 
867
| CT_letin(x1, x2) ->
 
868
   fDEF x1 ++
 
869
   fFORMULA x2 ++
 
870
   fNODE "letin" 2
 
871
| CT_notation(x1, x2) ->
 
872
   fSTRING x1 ++
 
873
   fFORMULA_LIST x2 ++
 
874
   fNODE "notation" 2
 
875
| CT_num_encapsulator(x1, x2) ->
 
876
   fNUM_TYPE x1 ++
 
877
   fFORMULA x2 ++
 
878
   fNODE "num_encapsulator" 2
 
879
| CT_prodc(x1, x2) ->
 
880
   fBINDER_NE_LIST x1 ++
 
881
   fFORMULA x2 ++
 
882
   fNODE "prodc" 2
 
883
| CT_proj(x1, x2) ->
 
884
   fFORMULA x1 ++
 
885
   fFORMULA_NE_LIST x2 ++
 
886
   fNODE "proj" 2
 
887
and fFORMULA_LIST = function
 
888
| CT_formula_list l ->
 
889
   (List.fold_left (++) (mt()) (List.map fFORMULA l)) ++
 
890
   fNODE "formula_list" (List.length l)
 
891
and fFORMULA_NE_LIST = function
 
892
| CT_formula_ne_list(x,l) ->
 
893
   fFORMULA x ++
 
894
   (List.fold_left (++) (mt()) (List.map fFORMULA l)) ++
 
895
   fNODE "formula_ne_list" (1 + (List.length l))
 
896
and fFORMULA_OPT = function
 
897
| CT_coerce_FORMULA_to_FORMULA_OPT x -> fFORMULA x
 
898
| CT_coerce_ID_OPT_to_FORMULA_OPT x -> fID_OPT x
 
899
and fFORMULA_OR_INT = function
 
900
| CT_coerce_FORMULA_to_FORMULA_OR_INT x -> fFORMULA x
 
901
| CT_coerce_ID_OR_INT_to_FORMULA_OR_INT x -> fID_OR_INT x
 
902
and fGRAMMAR = function
 
903
| CT_grammar_none -> fNODE "grammar_none" 0
 
904
and fHYP_LOCATION = function
 
905
| CT_coerce_UNFOLD_to_HYP_LOCATION x -> fUNFOLD x
 
906
| CT_intype(x1, x2) ->
 
907
   fID x1 ++
 
908
   fINT_LIST x2 ++
 
909
   fNODE "intype" 2
 
910
| CT_invalue(x1, x2) ->
 
911
   fID x1 ++
 
912
   fINT_LIST x2 ++
 
913
   fNODE "invalue" 2
 
914
and fHYP_LOCATION_LIST_OR_STAR = function
 
915
| CT_coerce_STAR_to_HYP_LOCATION_LIST_OR_STAR x -> fSTAR x
 
916
| CT_hyp_location_list l ->
 
917
   (List.fold_left (++) (mt()) (List.map fHYP_LOCATION l)) ++
 
918
   fNODE "hyp_location_list" (List.length l)
 
919
and fID = function
 
920
| CT_ident x -> fATOM "ident" ++
 
921
   (f_atom_string x) ++
 
922
   str "\n"
 
923
| CT_metac(x1) ->
 
924
   fINT x1 ++
 
925
   fNODE "metac" 1
 
926
| CT_metaid x -> fATOM "metaid" ++
 
927
   (f_atom_string x) ++
 
928
   str "\n"
 
929
and fIDENTITY_OPT = function
 
930
| CT_coerce_NONE_to_IDENTITY_OPT x -> fNONE x
 
931
| CT_identity -> fNODE "identity" 0
 
932
and fID_LIST = function
 
933
| CT_id_list l ->
 
934
   (List.fold_left (++) (mt()) (List.map fID l)) ++
 
935
   fNODE "id_list" (List.length l)
 
936
and fID_LIST_LIST = function
 
937
| CT_id_list_list l ->
 
938
   (List.fold_left (++) (mt()) (List.map fID_LIST l)) ++
 
939
   fNODE "id_list_list" (List.length l)
 
940
and fID_LIST_OPT = function
 
941
| CT_coerce_ID_LIST_to_ID_LIST_OPT x -> fID_LIST x
 
942
| CT_coerce_NONE_to_ID_LIST_OPT x -> fNONE x
 
943
and fID_NE_LIST = function
 
944
| CT_id_ne_list(x,l) ->
 
945
   fID x ++
 
946
   (List.fold_left (++) (mt()) (List.map fID l)) ++
 
947
   fNODE "id_ne_list" (1 + (List.length l))
 
948
and fID_NE_LIST_OR_STAR = function
 
949
| CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR x -> fID_NE_LIST x
 
950
| CT_coerce_STAR_to_ID_NE_LIST_OR_STAR x -> fSTAR x
 
951
and fID_NE_LIST_OR_STRING = function
 
952
| CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STRING x -> fID_NE_LIST x
 
953
| CT_coerce_STRING_to_ID_NE_LIST_OR_STRING x -> fSTRING x
 
954
and fID_OPT = function
 
955
| CT_coerce_ID_to_ID_OPT x -> fID x
 
956
| CT_coerce_NONE_to_ID_OPT x -> fNONE x
 
957
and fID_OPT_LIST = function
 
958
| CT_id_opt_list l ->
 
959
   (List.fold_left (++) (mt()) (List.map fID_OPT l)) ++
 
960
   fNODE "id_opt_list" (List.length l)
 
961
and fID_OPT_NE_LIST = function
 
962
| CT_id_opt_ne_list(x,l) ->
 
963
   fID_OPT x ++
 
964
   (List.fold_left (++) (mt()) (List.map fID_OPT l)) ++
 
965
   fNODE "id_opt_ne_list" (1 + (List.length l))
 
966
and fID_OPT_OR_ALL = function
 
967
| CT_coerce_ID_OPT_to_ID_OPT_OR_ALL x -> fID_OPT x
 
968
| CT_all -> fNODE "all" 0
 
969
and fID_OR_INT = function
 
970
| CT_coerce_ID_to_ID_OR_INT x -> fID x
 
971
| CT_coerce_INT_to_ID_OR_INT x -> fINT x
 
972
and fID_OR_INT_OPT = function
 
973
| CT_coerce_ID_OPT_to_ID_OR_INT_OPT x -> fID_OPT x
 
974
| CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT x -> fID_OR_INT x
 
975
| CT_coerce_INT_OPT_to_ID_OR_INT_OPT x -> fINT_OPT x
 
976
and fID_OR_STAR = function
 
977
| CT_coerce_ID_to_ID_OR_STAR x -> fID x
 
978
| CT_coerce_STAR_to_ID_OR_STAR x -> fSTAR x
 
979
and fID_OR_STRING = function
 
980
| CT_coerce_ID_to_ID_OR_STRING x -> fID x
 
981
| CT_coerce_STRING_to_ID_OR_STRING x -> fSTRING x
 
982
and fID_OR_STRING_NE_LIST = function
 
983
| CT_id_or_string_ne_list(x,l) ->
 
984
   fID_OR_STRING x ++
 
985
   (List.fold_left (++) (mt()) (List.map fID_OR_STRING l)) ++
 
986
   fNODE "id_or_string_ne_list" (1 + (List.length l))
 
987
and fIMPEXP = function
 
988
| CT_coerce_NONE_to_IMPEXP x -> fNONE x
 
989
| CT_export -> fNODE "export" 0
 
990
| CT_import -> fNODE "import" 0
 
991
and fIND_SPEC = function
 
992
| CT_ind_spec(x1, x2, x3, x4, x5) ->
 
993
   fID x1 ++
 
994
   fBINDER_LIST x2 ++
 
995
   fFORMULA x3 ++
 
996
   fCONSTR_LIST x4 ++
 
997
   fDECL_NOTATION_OPT x5 ++
 
998
   fNODE "ind_spec" 5
 
999
and fIND_SPEC_LIST = function
 
1000
| CT_ind_spec_list l ->
 
1001
   (List.fold_left (++) (mt()) (List.map fIND_SPEC l)) ++
 
1002
   fNODE "ind_spec_list" (List.length l)
 
1003
and fINT = function
 
1004
| CT_int x -> fATOM "int" ++
 
1005
   (f_atom_int x) ++
 
1006
   str "\n"
 
1007
and fINTRO_PATT = function
 
1008
| CT_coerce_ID_to_INTRO_PATT x -> fID x
 
1009
| CT_disj_pattern(x,l) ->
 
1010
   fINTRO_PATT_LIST x ++
 
1011
   (List.fold_left (++) (mt()) (List.map fINTRO_PATT_LIST l)) ++
 
1012
   fNODE "disj_pattern" (1 + (List.length l))
 
1013
and fINTRO_PATT_LIST = function
 
1014
| CT_intro_patt_list l ->
 
1015
   (List.fold_left (++) (mt()) (List.map fINTRO_PATT l)) ++
 
1016
   fNODE "intro_patt_list" (List.length l)
 
1017
and fINTRO_PATT_OPT = function
 
1018
| CT_coerce_ID_OPT_to_INTRO_PATT_OPT x -> fID_OPT x
 
1019
| CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT x -> fINTRO_PATT x
 
1020
and fINT_LIST = function
 
1021
| CT_int_list l ->
 
1022
   (List.fold_left (++) (mt()) (List.map fINT l)) ++
 
1023
   fNODE "int_list" (List.length l)
 
1024
and fINT_NE_LIST = function
 
1025
| CT_int_ne_list(x,l) ->
 
1026
   fINT x ++
 
1027
   (List.fold_left (++) (mt()) (List.map fINT l)) ++
 
1028
   fNODE "int_ne_list" (1 + (List.length l))
 
1029
and fINT_OPT = function
 
1030
| CT_coerce_INT_to_INT_OPT x -> fINT x
 
1031
| CT_coerce_NONE_to_INT_OPT x -> fNONE x
 
1032
and fINT_OR_LOCN = function
 
1033
| CT_coerce_INT_to_INT_OR_LOCN x -> fINT x
 
1034
| CT_coerce_LOCN_to_INT_OR_LOCN x -> fLOCN x
 
1035
and fINT_OR_NEXT = function
 
1036
| CT_coerce_INT_to_INT_OR_NEXT x -> fINT x
 
1037
| CT_next_level -> fNODE "next_level" 0
 
1038
and fINV_TYPE = function
 
1039
| CT_inv_clear -> fNODE "inv_clear" 0
 
1040
| CT_inv_regular -> fNODE "inv_regular" 0
 
1041
| CT_inv_simple -> fNODE "inv_simple" 0
 
1042
and fIN_OR_OUT_MODULES = function
 
1043
| CT_coerce_NONE_to_IN_OR_OUT_MODULES x -> fNONE x
 
1044
| CT_in_modules(x1) ->
 
1045
   fID_NE_LIST x1 ++
 
1046
   fNODE "in_modules" 1
 
1047
| CT_out_modules(x1) ->
 
1048
   fID_NE_LIST x1 ++
 
1049
   fNODE "out_modules" 1
 
1050
and fLET_CLAUSE = function
 
1051
| CT_let_clause(x1, x2, x3) ->
 
1052
   fID x1 ++
 
1053
   fTACTIC_OPT x2 ++
 
1054
   fLET_VALUE x3 ++
 
1055
   fNODE "let_clause" 3
 
1056
and fLET_CLAUSES = function
 
1057
| CT_let_clauses(x,l) ->
 
1058
   fLET_CLAUSE x ++
 
1059
   (List.fold_left (++) (mt()) (List.map fLET_CLAUSE l)) ++
 
1060
   fNODE "let_clauses" (1 + (List.length l))
 
1061
and fLET_VALUE = function
 
1062
| CT_coerce_DEF_BODY_to_LET_VALUE x -> fDEF_BODY x
 
1063
| CT_coerce_TACTIC_COM_to_LET_VALUE x -> fTACTIC_COM x
 
1064
and fLOCAL_OPT = function
 
1065
| CT_coerce_NONE_to_LOCAL_OPT x -> fNONE x
 
1066
| CT_local -> fNODE "local" 0
 
1067
and fLOCN = function
 
1068
| CT_locn x -> fATOM "locn" ++
 
1069
   (f_atom_string x) ++
 
1070
   str "\n"
 
1071
and fMATCHED_FORMULA = function
 
1072
| CT_coerce_FORMULA_to_MATCHED_FORMULA x -> fFORMULA x
 
1073
| CT_formula_as(x1, x2) ->
 
1074
   fFORMULA x1 ++
 
1075
   fID_OPT x2 ++
 
1076
   fNODE "formula_as" 2
 
1077
| CT_formula_as_in(x1, x2, x3) ->
 
1078
   fFORMULA x1 ++
 
1079
   fID_OPT x2 ++
 
1080
   fFORMULA x3 ++
 
1081
   fNODE "formula_as_in" 3
 
1082
| CT_formula_in(x1, x2) ->
 
1083
   fFORMULA x1 ++
 
1084
   fFORMULA x2 ++
 
1085
   fNODE "formula_in" 2
 
1086
and fMATCHED_FORMULA_NE_LIST = function
 
1087
| CT_matched_formula_ne_list(x,l) ->
 
1088
   fMATCHED_FORMULA x ++
 
1089
   (List.fold_left (++) (mt()) (List.map fMATCHED_FORMULA l)) ++
 
1090
   fNODE "matched_formula_ne_list" (1 + (List.length l))
 
1091
and fMATCH_PATTERN = function
 
1092
| CT_coerce_ID_OPT_to_MATCH_PATTERN x -> fID_OPT x
 
1093
| CT_coerce_NUM_to_MATCH_PATTERN x -> fNUM x
 
1094
| CT_pattern_app(x1, x2) ->
 
1095
   fMATCH_PATTERN x1 ++
 
1096
   fMATCH_PATTERN_NE_LIST x2 ++
 
1097
   fNODE "pattern_app" 2
 
1098
| CT_pattern_as(x1, x2) ->
 
1099
   fMATCH_PATTERN x1 ++
 
1100
   fID_OPT x2 ++
 
1101
   fNODE "pattern_as" 2
 
1102
| CT_pattern_delimitors(x1, x2) ->
 
1103
   fNUM_TYPE x1 ++
 
1104
   fMATCH_PATTERN x2 ++
 
1105
   fNODE "pattern_delimitors" 2
 
1106
| CT_pattern_notation(x1, x2) ->
 
1107
   fSTRING x1 ++
 
1108
   fMATCH_PATTERN_LIST x2 ++
 
1109
   fNODE "pattern_notation" 2
 
1110
and fMATCH_PATTERN_LIST = function
 
1111
| CT_match_pattern_list l ->
 
1112
   (List.fold_left (++) (mt()) (List.map fMATCH_PATTERN l)) ++
 
1113
   fNODE "match_pattern_list" (List.length l)
 
1114
and fMATCH_PATTERN_NE_LIST = function
 
1115
| CT_match_pattern_ne_list(x,l) ->
 
1116
   fMATCH_PATTERN x ++
 
1117
   (List.fold_left (++) (mt()) (List.map fMATCH_PATTERN l)) ++
 
1118
   fNODE "match_pattern_ne_list" (1 + (List.length l))
 
1119
and fMATCH_TAC_RULE = function
 
1120
| CT_match_tac_rule(x1, x2) ->
 
1121
   fCONTEXT_PATTERN x1 ++
 
1122
   fLET_VALUE x2 ++
 
1123
   fNODE "match_tac_rule" 2
 
1124
and fMATCH_TAC_RULES = function
 
1125
| CT_match_tac_rules(x,l) ->
 
1126
   fMATCH_TAC_RULE x ++
 
1127
   (List.fold_left (++) (mt()) (List.map fMATCH_TAC_RULE l)) ++
 
1128
   fNODE "match_tac_rules" (1 + (List.length l))
 
1129
and fMODIFIER = function
 
1130
| CT_entry_type(x1, x2) ->
 
1131
   fID x1 ++
 
1132
   fID x2 ++
 
1133
   fNODE "entry_type" 2
 
1134
| CT_format(x1) ->
 
1135
   fSTRING x1 ++
 
1136
   fNODE "format" 1
 
1137
| CT_lefta -> fNODE "lefta" 0
 
1138
| CT_nona -> fNODE "nona" 0
 
1139
| CT_only_parsing -> fNODE "only_parsing" 0
 
1140
| CT_righta -> fNODE "righta" 0
 
1141
| CT_set_item_level(x1, x2) ->
 
1142
   fID_NE_LIST x1 ++
 
1143
   fINT_OR_NEXT x2 ++
 
1144
   fNODE "set_item_level" 2
 
1145
| CT_set_level(x1) ->
 
1146
   fINT x1 ++
 
1147
   fNODE "set_level" 1
 
1148
and fMODIFIER_LIST = function
 
1149
| CT_modifier_list l ->
 
1150
   (List.fold_left (++) (mt()) (List.map fMODIFIER l)) ++
 
1151
   fNODE "modifier_list" (List.length l)
 
1152
and fMODULE_BINDER = function
 
1153
| CT_module_binder(x1, x2) ->
 
1154
   fID_NE_LIST x1 ++
 
1155
   fMODULE_TYPE x2 ++
 
1156
   fNODE "module_binder" 2
 
1157
and fMODULE_BINDER_LIST = function
 
1158
| CT_module_binder_list l ->
 
1159
   (List.fold_left (++) (mt()) (List.map fMODULE_BINDER l)) ++
 
1160
   fNODE "module_binder_list" (List.length l)
 
1161
and fMODULE_EXPR = function
 
1162
| CT_coerce_ID_OPT_to_MODULE_EXPR x -> fID_OPT x
 
1163
| CT_module_app(x1, x2) ->
 
1164
   fMODULE_EXPR x1 ++
 
1165
   fMODULE_EXPR x2 ++
 
1166
   fNODE "module_app" 2
 
1167
and fMODULE_TYPE = function
 
1168
| CT_coerce_ID_to_MODULE_TYPE x -> fID x
 
1169
| CT_module_type_with_def(x1, x2, x3) ->
 
1170
   fMODULE_TYPE x1 ++
 
1171
   fID_LIST x2 ++
 
1172
   fFORMULA x3 ++
 
1173
   fNODE "module_type_with_def" 3
 
1174
| CT_module_type_with_mod(x1, x2, x3) ->
 
1175
   fMODULE_TYPE x1 ++
 
1176
   fID_LIST x2 ++
 
1177
   fID x3 ++
 
1178
   fNODE "module_type_with_mod" 3
 
1179
and fMODULE_TYPE_CHECK = function
 
1180
| CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK x -> fMODULE_TYPE_OPT x
 
1181
| CT_only_check(x1) ->
 
1182
   fMODULE_TYPE x1 ++
 
1183
   fNODE "only_check" 1
 
1184
and fMODULE_TYPE_OPT = function
 
1185
| CT_coerce_ID_OPT_to_MODULE_TYPE_OPT x -> fID_OPT x
 
1186
| CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT x -> fMODULE_TYPE x
 
1187
and fNATURAL_FEATURE = function
 
1188
| CT_contractible -> fNODE "contractible" 0
 
1189
| CT_implicit -> fNODE "implicit" 0
 
1190
| CT_nat_transparent -> fNODE "nat_transparent" 0
 
1191
and fNONE = function
 
1192
| CT_none -> fNODE "none" 0
 
1193
and fNUM = function
 
1194
| CT_int_encapsulator x -> fATOM "int_encapsulator" ++
 
1195
   (f_atom_string x) ++
 
1196
   str "\n"
 
1197
and fNUM_TYPE = function
 
1198
| CT_num_type x -> fATOM "num_type" ++
 
1199
   (f_atom_string x) ++
 
1200
   str "\n"
 
1201
and fOMEGA_FEATURE = function
 
1202
| CT_coerce_STRING_to_OMEGA_FEATURE x -> fSTRING x
 
1203
| CT_flag_action -> fNODE "flag_action" 0
 
1204
| CT_flag_system -> fNODE "flag_system" 0
 
1205
| CT_flag_time -> fNODE "flag_time" 0
 
1206
and fOMEGA_MODE = function
 
1207
| CT_set -> fNODE "set" 0
 
1208
| CT_switch -> fNODE "switch" 0
 
1209
| CT_unset -> fNODE "unset" 0
 
1210
and fORIENTATION = function
 
1211
| CT_lr -> fNODE "lr" 0
 
1212
| CT_rl -> fNODE "rl" 0
 
1213
and fPATTERN = function
 
1214
| CT_pattern_occ(x1, x2) ->
 
1215
   fINT_LIST x1 ++
 
1216
   fFORMULA x2 ++
 
1217
   fNODE "pattern_occ" 2
 
1218
and fPATTERN_NE_LIST = function
 
1219
| CT_pattern_ne_list(x,l) ->
 
1220
   fPATTERN x ++
 
1221
   (List.fold_left (++) (mt()) (List.map fPATTERN l)) ++
 
1222
   fNODE "pattern_ne_list" (1 + (List.length l))
 
1223
and fPATTERN_OPT = function
 
1224
| CT_coerce_NONE_to_PATTERN_OPT x -> fNONE x
 
1225
| CT_coerce_PATTERN_to_PATTERN_OPT x -> fPATTERN x
 
1226
and fPREMISE = function
 
1227
| CT_coerce_TYPED_FORMULA_to_PREMISE x -> fTYPED_FORMULA x
 
1228
| CT_eval_result(x1, x2, x3) ->
 
1229
   fFORMULA x1 ++
 
1230
   fFORMULA x2 ++
 
1231
   fFORMULA x3 ++
 
1232
   fNODE "eval_result" 3
 
1233
| CT_premise(x1, x2) ->
 
1234
   fID x1 ++
 
1235
   fFORMULA x2 ++
 
1236
   fNODE "premise" 2
 
1237
and fPREMISES_LIST = function
 
1238
| CT_premises_list l ->
 
1239
   (List.fold_left (++) (mt()) (List.map fPREMISE l)) ++
 
1240
   fNODE "premises_list" (List.length l)
 
1241
and fPREMISE_PATTERN = function
 
1242
| CT_premise_pattern(x1, x2) ->
 
1243
   fID_OPT x1 ++
 
1244
   fCONTEXT_PATTERN x2 ++
 
1245
   fNODE "premise_pattern" 2
 
1246
and fPROOF_SCRIPT = function
 
1247
| CT_proof_script l ->
 
1248
   (List.fold_left (++) (mt()) (List.map fCOMMAND l)) ++
 
1249
   fNODE "proof_script" (List.length l)
 
1250
and fRECCONSTR = function
 
1251
| CT_defrecconstr(x1, x2, x3) ->
 
1252
   fID_OPT x1 ++
 
1253
   fFORMULA x2 ++
 
1254
   fFORMULA_OPT x3 ++
 
1255
   fNODE "defrecconstr" 3
 
1256
| CT_defrecconstr_coercion(x1, x2, x3) ->
 
1257
   fID_OPT x1 ++
 
1258
   fFORMULA x2 ++
 
1259
   fFORMULA_OPT x3 ++
 
1260
   fNODE "defrecconstr_coercion" 3
 
1261
| CT_recconstr(x1, x2) ->
 
1262
   fID_OPT x1 ++
 
1263
   fFORMULA x2 ++
 
1264
   fNODE "recconstr" 2
 
1265
| CT_recconstr_coercion(x1, x2) ->
 
1266
   fID_OPT x1 ++
 
1267
   fFORMULA x2 ++
 
1268
   fNODE "recconstr_coercion" 2
 
1269
and fRECCONSTR_LIST = function
 
1270
| CT_recconstr_list l ->
 
1271
   (List.fold_left (++) (mt()) (List.map fRECCONSTR l)) ++
 
1272
   fNODE "recconstr_list" (List.length l)
 
1273
and fREC_TACTIC_FUN = function
 
1274
| CT_rec_tactic_fun(x1, x2, x3) ->
 
1275
   fID x1 ++
 
1276
   fID_OPT_NE_LIST x2 ++
 
1277
   fTACTIC_COM x3 ++
 
1278
   fNODE "rec_tactic_fun" 3
 
1279
and fREC_TACTIC_FUN_LIST = function
 
1280
| CT_rec_tactic_fun_list(x,l) ->
 
1281
   fREC_TACTIC_FUN x ++
 
1282
   (List.fold_left (++) (mt()) (List.map fREC_TACTIC_FUN l)) ++
 
1283
   fNODE "rec_tactic_fun_list" (1 + (List.length l))
 
1284
and fRED_COM = function
 
1285
| CT_cbv(x1, x2) ->
 
1286
   fCONVERSION_FLAG_LIST x1 ++
 
1287
   fCONV_SET x2 ++
 
1288
   fNODE "cbv" 2
 
1289
| CT_fold(x1) ->
 
1290
   fFORMULA_LIST x1 ++
 
1291
   fNODE "fold" 1
 
1292
| CT_hnf -> fNODE "hnf" 0
 
1293
| CT_lazy(x1, x2) ->
 
1294
   fCONVERSION_FLAG_LIST x1 ++
 
1295
   fCONV_SET x2 ++
 
1296
   fNODE "lazy" 2
 
1297
| CT_pattern(x1) ->
 
1298
   fPATTERN_NE_LIST x1 ++
 
1299
   fNODE "pattern" 1
 
1300
| CT_red -> fNODE "red" 0
 
1301
| CT_cbvvm -> fNODE "vm_compute" 0
 
1302
| CT_simpl(x1) ->
 
1303
   fPATTERN_OPT x1 ++
 
1304
   fNODE "simpl" 1
 
1305
| CT_unfold(x1) ->
 
1306
   fUNFOLD_NE_LIST x1 ++
 
1307
   fNODE "unfold" 1
 
1308
and fRETURN_INFO = function
 
1309
| CT_coerce_NONE_to_RETURN_INFO x -> fNONE x
 
1310
| CT_as_and_return(x1, x2) ->
 
1311
   fID_OPT x1 ++
 
1312
   fFORMULA x2 ++
 
1313
   fNODE "as_and_return" 2
 
1314
| CT_return(x1) ->
 
1315
   fFORMULA x1 ++
 
1316
   fNODE "return" 1
 
1317
and fRULE = function
 
1318
| CT_rule(x1, x2) ->
 
1319
   fPREMISES_LIST x1 ++
 
1320
   fFORMULA x2 ++
 
1321
   fNODE "rule" 2
 
1322
and fRULE_LIST = function
 
1323
| CT_rule_list l ->
 
1324
   (List.fold_left (++) (mt()) (List.map fRULE l)) ++
 
1325
   fNODE "rule_list" (List.length l)
 
1326
and fSCHEME_SPEC = function
 
1327
| CT_scheme_spec(x1, x2, x3, x4) ->
 
1328
   fID x1 ++
 
1329
   fDEP x2 ++
 
1330
   fFORMULA x3 ++
 
1331
   fSORT_TYPE x4 ++
 
1332
   fNODE "scheme_spec" 4
 
1333
and fSCHEME_SPEC_LIST = function
 
1334
| CT_scheme_spec_list(x,l) ->
 
1335
   fSCHEME_SPEC x ++
 
1336
   (List.fold_left (++) (mt()) (List.map fSCHEME_SPEC l)) ++
 
1337
   fNODE "scheme_spec_list" (1 + (List.length l))
 
1338
and fSCOMMENT_CONTENT = function
 
1339
| CT_coerce_FORMULA_to_SCOMMENT_CONTENT x -> fFORMULA x
 
1340
| CT_coerce_ID_OR_STRING_to_SCOMMENT_CONTENT x -> fID_OR_STRING x
 
1341
and fSCOMMENT_CONTENT_LIST = function
 
1342
| CT_scomment_content_list l ->
 
1343
   (List.fold_left (++) (mt()) (List.map fSCOMMENT_CONTENT l)) ++
 
1344
   fNODE "scomment_content_list" (List.length l)
 
1345
and fSECTION_BEGIN = function
 
1346
| CT_section(x1) ->
 
1347
   fID x1 ++
 
1348
   fNODE "section" 1
 
1349
and fSECTION_BODY = function
 
1350
| CT_section_body l ->
 
1351
   (List.fold_left (++) (mt()) (List.map fCOMMAND l)) ++
 
1352
   fNODE "section_body" (List.length l)
 
1353
and fSIGNED_INT = function
 
1354
| CT_coerce_INT_to_SIGNED_INT x -> fINT x
 
1355
| CT_minus(x1) ->
 
1356
   fINT x1 ++
 
1357
   fNODE "minus" 1
 
1358
and fSIGNED_INT_LIST = function
 
1359
| CT_signed_int_list l ->
 
1360
   (List.fold_left (++) (mt()) (List.map fSIGNED_INT l)) ++
 
1361
   fNODE "signed_int_list" (List.length l)
 
1362
and fSINGLE_OPTION_VALUE = function
 
1363
| CT_coerce_INT_to_SINGLE_OPTION_VALUE x -> fINT x
 
1364
| CT_coerce_STRING_to_SINGLE_OPTION_VALUE x -> fSTRING x
 
1365
and fSORT_TYPE = function
 
1366
| CT_sortc x -> fATOM "sortc" ++
 
1367
   (f_atom_string x) ++
 
1368
   str "\n"
 
1369
and fSPEC_LIST = function
 
1370
| CT_coerce_BINDING_LIST_to_SPEC_LIST x -> fBINDING_LIST x
 
1371
| CT_coerce_FORMULA_LIST_to_SPEC_LIST x -> fFORMULA_LIST x
 
1372
and fSPEC_OPT = function
 
1373
| CT_coerce_NONE_to_SPEC_OPT x -> fNONE x
 
1374
| CT_spec -> fNODE "spec" 0
 
1375
and fSTAR = function
 
1376
| CT_star -> fNODE "star" 0
 
1377
and fSTAR_OPT = function
 
1378
| CT_coerce_NONE_to_STAR_OPT x -> fNONE x
 
1379
| CT_coerce_STAR_to_STAR_OPT x -> fSTAR x
 
1380
and fSTRING = function
 
1381
| CT_string x -> fATOM "string" ++
 
1382
   (f_atom_string x) ++
 
1383
   str "\n"
 
1384
and fSTRING_NE_LIST = function
 
1385
| CT_string_ne_list(x,l) ->
 
1386
   fSTRING x ++
 
1387
   (List.fold_left (++) (mt()) (List.map fSTRING l)) ++
 
1388
   fNODE "string_ne_list" (1 + (List.length l))
 
1389
and fSTRING_OPT = function
 
1390
| CT_coerce_NONE_to_STRING_OPT x -> fNONE x
 
1391
| CT_coerce_STRING_to_STRING_OPT x -> fSTRING x
 
1392
and fTABLE = function
 
1393
| CT_coerce_ID_to_TABLE x -> fID x
 
1394
| CT_table(x1, x2) ->
 
1395
   fID x1 ++
 
1396
   fID x2 ++
 
1397
   fNODE "table" 2
 
1398
and fTACTIC_ARG = function
 
1399
| CT_coerce_EVAL_CMD_to_TACTIC_ARG x -> fEVAL_CMD x
 
1400
| CT_coerce_FORMULA_OR_INT_to_TACTIC_ARG x -> fFORMULA_OR_INT x
 
1401
| CT_coerce_TACTIC_COM_to_TACTIC_ARG x -> fTACTIC_COM x
 
1402
| CT_coerce_TERM_CHANGE_to_TACTIC_ARG x -> fTERM_CHANGE x
 
1403
| CT_void -> fNODE "void" 0
 
1404
and fTACTIC_ARG_LIST = function
 
1405
| CT_tactic_arg_list(x,l) ->
 
1406
   fTACTIC_ARG x ++
 
1407
   (List.fold_left (++) (mt()) (List.map fTACTIC_ARG l)) ++
 
1408
   fNODE "tactic_arg_list" (1 + (List.length l))
 
1409
and fTACTIC_COM = function
 
1410
| CT_abstract(x1, x2) ->
 
1411
   fID_OPT x1 ++
 
1412
   fTACTIC_COM x2 ++
 
1413
   fNODE "abstract" 2
 
1414
| CT_absurd(x1) ->
 
1415
   fFORMULA x1 ++
 
1416
   fNODE "absurd" 1
 
1417
| CT_any_constructor(x1) ->
 
1418
   fTACTIC_OPT x1 ++
 
1419
   fNODE "any_constructor" 1
 
1420
| CT_apply(x1, x2) ->
 
1421
   fFORMULA x1 ++
 
1422
   fSPEC_LIST x2 ++
 
1423
   fNODE "apply" 2
 
1424
| CT_assert(x1, x2) ->
 
1425
   fID_OPT x1 ++
 
1426
   fFORMULA x2 ++
 
1427
   fNODE "assert" 2
 
1428
| CT_assumption -> fNODE "assumption" 0
 
1429
| CT_auto(x1) ->
 
1430
   fINT_OPT x1 ++
 
1431
   fNODE "auto" 1
 
1432
| CT_auto_with(x1, x2) ->
 
1433
   fINT_OPT x1 ++
 
1434
   fID_NE_LIST_OR_STAR x2 ++
 
1435
   fNODE "auto_with" 2
 
1436
| CT_autorewrite(x1, x2) ->
 
1437
   fID_NE_LIST x1 ++
 
1438
   fTACTIC_OPT x2 ++
 
1439
   fNODE "autorewrite" 2
 
1440
| CT_autotdb(x1) ->
 
1441
   fINT_OPT x1 ++
 
1442
   fNODE "autotdb" 1
 
1443
| CT_case_type(x1) ->
 
1444
   fFORMULA x1 ++
 
1445
   fNODE "case_type" 1
 
1446
| CT_casetac(x1, x2) ->
 
1447
   fFORMULA x1 ++
 
1448
   fSPEC_LIST x2 ++
 
1449
   fNODE "casetac" 2
 
1450
| CT_cdhyp(x1) ->
 
1451
   fID x1 ++
 
1452
   fNODE "cdhyp" 1
 
1453
| CT_change(x1, x2) ->
 
1454
   fFORMULA x1 ++
 
1455
   fCLAUSE x2 ++
 
1456
   fNODE "change" 2
 
1457
| CT_change_local(x1, x2, x3) ->
 
1458
   fPATTERN x1 ++
 
1459
   fFORMULA x2 ++
 
1460
   fCLAUSE x3 ++
 
1461
   fNODE "change_local" 3
 
1462
| CT_clear(x1) ->
 
1463
   fID_NE_LIST x1 ++
 
1464
   fNODE "clear" 1
 
1465
| CT_clear_body(x1) ->
 
1466
   fID_NE_LIST x1 ++
 
1467
   fNODE "clear_body" 1
 
1468
| CT_cofixtactic(x1, x2) ->
 
1469
   fID_OPT x1 ++
 
1470
   fCOFIX_TAC_LIST x2 ++
 
1471
   fNODE "cofixtactic" 2
 
1472
| CT_condrewrite_lr(x1, x2, x3, x4) ->
 
1473
   fTACTIC_COM x1 ++
 
1474
   fFORMULA x2 ++
 
1475
   fSPEC_LIST x3 ++
 
1476
   fID_OPT x4 ++
 
1477
   fNODE "condrewrite_lr" 4
 
1478
| CT_condrewrite_rl(x1, x2, x3, x4) ->
 
1479
   fTACTIC_COM x1 ++
 
1480
   fFORMULA x2 ++
 
1481
   fSPEC_LIST x3 ++
 
1482
   fID_OPT x4 ++
 
1483
   fNODE "condrewrite_rl" 4
 
1484
| CT_constructor(x1, x2) ->
 
1485
   fINT x1 ++
 
1486
   fSPEC_LIST x2 ++
 
1487
   fNODE "constructor" 2
 
1488
| CT_contradiction -> fNODE "contradiction" 0
 
1489
| CT_contradiction_thm(x1, x2) ->
 
1490
   fFORMULA x1 ++
 
1491
   fSPEC_LIST x2 ++
 
1492
   fNODE "contradiction_thm" 2
 
1493
| CT_cut(x1) ->
 
1494
   fFORMULA x1 ++
 
1495
   fNODE "cut" 1
 
1496
| CT_cutrewrite_lr(x1, x2) ->
 
1497
   fFORMULA x1 ++
 
1498
   fID_OPT x2 ++
 
1499
   fNODE "cutrewrite_lr" 2
 
1500
| CT_cutrewrite_rl(x1, x2) ->
 
1501
   fFORMULA x1 ++
 
1502
   fID_OPT x2 ++
 
1503
   fNODE "cutrewrite_rl" 2
 
1504
| CT_dauto(x1, x2) ->
 
1505
   fINT_OPT x1 ++
 
1506
   fINT_OPT x2 ++
 
1507
   fNODE "dauto" 2
 
1508
| CT_dconcl -> fNODE "dconcl" 0
 
1509
| CT_decompose_list(x1, x2) ->
 
1510
   fID_NE_LIST x1 ++
 
1511
   fFORMULA x2 ++
 
1512
   fNODE "decompose_list" 2
 
1513
| CT_decompose_record(x1) ->
 
1514
   fFORMULA x1 ++
 
1515
   fNODE "decompose_record" 1
 
1516
| CT_decompose_sum(x1) ->
 
1517
   fFORMULA x1 ++
 
1518
   fNODE "decompose_sum" 1
 
1519
| CT_depinversion(x1, x2, x3, x4) ->
 
1520
   fINV_TYPE x1 ++
 
1521
   fID_OR_INT x2 ++
 
1522
   fINTRO_PATT_OPT x3 ++
 
1523
   fFORMULA_OPT x4 ++
 
1524
   fNODE "depinversion" 4
 
1525
| CT_deprewrite_lr(x1) ->
 
1526
   fID x1 ++
 
1527
   fNODE "deprewrite_lr" 1
 
1528
| CT_deprewrite_rl(x1) ->
 
1529
   fID x1 ++
 
1530
   fNODE "deprewrite_rl" 1
 
1531
| CT_destruct(x1) ->
 
1532
   fID_OR_INT x1 ++
 
1533
   fNODE "destruct" 1
 
1534
| CT_dhyp(x1) ->
 
1535
   fID x1 ++
 
1536
   fNODE "dhyp" 1
 
1537
| CT_discriminate_eq(x1) ->
 
1538
   fID_OR_INT_OPT x1 ++
 
1539
   fNODE "discriminate_eq" 1
 
1540
| CT_do(x1, x2) ->
 
1541
   fID_OR_INT x1 ++
 
1542
   fTACTIC_COM x2 ++
 
1543
   fNODE "do" 2
 
1544
| CT_eapply(x1, x2) ->
 
1545
   fFORMULA x1 ++
 
1546
   fSPEC_LIST x2 ++
 
1547
   fNODE "eapply" 2
 
1548
| CT_eauto(x1, x2) ->
 
1549
   fID_OR_INT_OPT x1 ++
 
1550
   fID_OR_INT_OPT x2 ++
 
1551
   fNODE "eauto" 2
 
1552
| CT_eauto_with(x1, x2, x3) ->
 
1553
   fID_OR_INT_OPT x1 ++
 
1554
   fID_OR_INT_OPT x2 ++
 
1555
   fID_NE_LIST_OR_STAR x3 ++
 
1556
   fNODE "eauto_with" 3
 
1557
| CT_elim(x1, x2, x3) ->
 
1558
   fFORMULA x1 ++
 
1559
   fSPEC_LIST x2 ++
 
1560
   fUSING x3 ++
 
1561
   fNODE "elim" 3
 
1562
| CT_elim_type(x1) ->
 
1563
   fFORMULA x1 ++
 
1564
   fNODE "elim_type" 1
 
1565
| CT_exact(x1) ->
 
1566
   fFORMULA x1 ++
 
1567
   fNODE "exact" 1
 
1568
| CT_exact_no_check(x1) ->
 
1569
   fFORMULA x1 ++
 
1570
   fNODE "exact_no_check" 1
 
1571
| CT_vm_cast_no_check(x1) ->
 
1572
   fFORMULA x1 ++
 
1573
   fNODE "vm_cast_no_check" 1
 
1574
| CT_exists(x1) ->
 
1575
   fSPEC_LIST x1 ++
 
1576
   fNODE "exists" 1
 
1577
| CT_fail(x1, x2) ->
 
1578
   fID_OR_INT x1 ++
 
1579
   fSTRING_OPT x2 ++
 
1580
   fNODE "fail" 2
 
1581
| CT_first(x,l) ->
 
1582
   fTACTIC_COM x ++
 
1583
   (List.fold_left (++) (mt()) (List.map fTACTIC_COM l)) ++
 
1584
   fNODE "first" (1 + (List.length l))
 
1585
| CT_firstorder(x1) ->
 
1586
   fTACTIC_OPT x1 ++
 
1587
   fNODE "firstorder" 1
 
1588
| CT_firstorder_using(x1, x2) ->
 
1589
   fTACTIC_OPT x1 ++
 
1590
   fID_NE_LIST x2 ++
 
1591
   fNODE "firstorder_using" 2
 
1592
| CT_firstorder_with(x1, x2) ->
 
1593
   fTACTIC_OPT x1 ++
 
1594
   fID_NE_LIST x2 ++
 
1595
   fNODE "firstorder_with" 2
 
1596
| CT_fixtactic(x1, x2, x3) ->
 
1597
   fID_OPT x1 ++
 
1598
   fINT x2 ++
 
1599
   fFIX_TAC_LIST x3 ++
 
1600
   fNODE "fixtactic" 3
 
1601
| CT_formula_marker(x1) ->
 
1602
   fFORMULA x1 ++
 
1603
   fNODE "formula_marker" 1
 
1604
| CT_fresh(x1) ->
 
1605
   fSTRING_OPT x1 ++
 
1606
   fNODE "fresh" 1
 
1607
| CT_generalize(x1) ->
 
1608
   fFORMULA_NE_LIST x1 ++
 
1609
   fNODE "generalize" 1
 
1610
| CT_generalize_dependent(x1) ->
 
1611
   fFORMULA x1 ++
 
1612
   fNODE "generalize_dependent" 1
 
1613
| CT_idtac(x1) ->
 
1614
   fSTRING_OPT x1 ++
 
1615
   fNODE "idtac" 1
 
1616
| CT_induction(x1) ->
 
1617
   fID_OR_INT x1 ++
 
1618
   fNODE "induction" 1
 
1619
| CT_info(x1) ->
 
1620
   fTACTIC_COM x1 ++
 
1621
   fNODE "info" 1
 
1622
| CT_injection_eq(x1) ->
 
1623
   fID_OR_INT_OPT x1 ++
 
1624
   fNODE "injection_eq" 1
 
1625
| CT_instantiate(x1, x2, x3) ->
 
1626
   fINT x1 ++
 
1627
   fFORMULA x2 ++
 
1628
   fCLAUSE x3 ++
 
1629
   fNODE "instantiate" 3
 
1630
| CT_intro(x1) ->
 
1631
   fID_OPT x1 ++
 
1632
   fNODE "intro" 1
 
1633
| CT_intro_after(x1, x2) ->
 
1634
   fID_OPT x1 ++
 
1635
   fID x2 ++
 
1636
   fNODE "intro_after" 2
 
1637
| CT_intros(x1) ->
 
1638
   fINTRO_PATT_LIST x1 ++
 
1639
   fNODE "intros" 1
 
1640
| CT_intros_until(x1) ->
 
1641
   fID_OR_INT x1 ++
 
1642
   fNODE "intros_until" 1
 
1643
| CT_inversion(x1, x2, x3, x4) ->
 
1644
   fINV_TYPE x1 ++
 
1645
   fID_OR_INT x2 ++
 
1646
   fINTRO_PATT_OPT x3 ++
 
1647
   fID_LIST x4 ++
 
1648
   fNODE "inversion" 4
 
1649
| CT_left(x1) ->
 
1650
   fSPEC_LIST x1 ++
 
1651
   fNODE "left" 1
 
1652
| CT_let_ltac(x1, x2) ->
 
1653
   fLET_CLAUSES x1 ++
 
1654
   fLET_VALUE x2 ++
 
1655
   fNODE "let_ltac" 2
 
1656
| CT_lettac(x1, x2, x3) ->
 
1657
   fID_OPT x1 ++
 
1658
   fFORMULA x2 ++
 
1659
   fCLAUSE x3 ++
 
1660
   fNODE "lettac" 3
 
1661
| CT_match_context(x,l) ->
 
1662
   fCONTEXT_RULE x ++
 
1663
   (List.fold_left (++) (mt()) (List.map fCONTEXT_RULE l)) ++
 
1664
   fNODE "match_context" (1 + (List.length l))
 
1665
| CT_match_context_reverse(x,l) ->
 
1666
   fCONTEXT_RULE x ++
 
1667
   (List.fold_left (++) (mt()) (List.map fCONTEXT_RULE l)) ++
 
1668
   fNODE "match_context_reverse" (1 + (List.length l))
 
1669
| CT_match_tac(x1, x2) ->
 
1670
   fTACTIC_COM x1 ++
 
1671
   fMATCH_TAC_RULES x2 ++
 
1672
   fNODE "match_tac" 2
 
1673
| CT_move_after(x1, x2) ->
 
1674
   fID x1 ++
 
1675
   fID x2 ++
 
1676
   fNODE "move_after" 2
 
1677
| CT_new_destruct(x1, x2, x3) ->
 
1678
   (List.fold_left (++) (mt()) (List.map fFORMULA_OR_INT x1)) ++ (* Julien F. Est-ce correct? *)
 
1679
   fUSING x2 ++
 
1680
   fINTRO_PATT_OPT x3 ++
 
1681
   fNODE "new_destruct" 3
 
1682
| CT_new_induction(x1, x2, x3) ->
 
1683
   (List.fold_left (++) (mt()) (List.map fFORMULA_OR_INT x1)) ++ (* Pierre C. Est-ce correct? *)
 
1684
   fUSING x2 ++
 
1685
   fINTRO_PATT_OPT x3 ++
 
1686
   fNODE "new_induction" 3
 
1687
| CT_omega -> fNODE "omega" 0
 
1688
| CT_orelse(x1, x2) ->
 
1689
   fTACTIC_COM x1 ++
 
1690
   fTACTIC_COM x2 ++
 
1691
   fNODE "orelse" 2
 
1692
| CT_parallel(x,l) ->
 
1693
   fTACTIC_COM x ++
 
1694
   (List.fold_left (++) (mt()) (List.map fTACTIC_COM l)) ++
 
1695
   fNODE "parallel" (1 + (List.length l))
 
1696
| CT_pose(x1, x2) ->
 
1697
   fID_OPT x1 ++
 
1698
   fFORMULA x2 ++
 
1699
   fNODE "pose" 2
 
1700
| CT_progress(x1) ->
 
1701
   fTACTIC_COM x1 ++
 
1702
   fNODE "progress" 1
 
1703
| CT_prolog(x1, x2) ->
 
1704
   fFORMULA_LIST x1 ++
 
1705
   fINT x2 ++
 
1706
   fNODE "prolog" 2
 
1707
| CT_rec_tactic_in(x1, x2) ->
 
1708
   fREC_TACTIC_FUN_LIST x1 ++
 
1709
   fTACTIC_COM x2 ++
 
1710
   fNODE "rec_tactic_in" 2
 
1711
| CT_reduce(x1, x2) ->
 
1712
   fRED_COM x1 ++
 
1713
   fCLAUSE x2 ++
 
1714
   fNODE "reduce" 2
 
1715
| CT_refine(x1) ->
 
1716
   fFORMULA x1 ++
 
1717
   fNODE "refine" 1
 
1718
| CT_reflexivity -> fNODE "reflexivity" 0
 
1719
| CT_rename(x1, x2) ->
 
1720
   fID x1 ++
 
1721
   fID x2 ++
 
1722
   fNODE "rename" 2
 
1723
| CT_repeat(x1) ->
 
1724
   fTACTIC_COM x1 ++
 
1725
   fNODE "repeat" 1
 
1726
| CT_replace_with(x1, x2,x3,x4) ->
 
1727
   fFORMULA x1 ++
 
1728
   fFORMULA x2 ++
 
1729
   fCLAUSE x3 ++
 
1730
   fTACTIC_OPT x4 ++
 
1731
   fNODE "replace_with" 4
 
1732
| CT_rewrite_lr(x1, x2, x3) ->
 
1733
   fFORMULA x1 ++
 
1734
   fSPEC_LIST x2 ++
 
1735
   fCLAUSE x3 ++
 
1736
   fNODE "rewrite_lr" 3
 
1737
| CT_rewrite_rl(x1, x2, x3) ->
 
1738
   fFORMULA x1 ++
 
1739
   fSPEC_LIST x2 ++
 
1740
   fCLAUSE x3 ++
 
1741
   fNODE "rewrite_rl" 3
 
1742
| CT_right(x1) ->
 
1743
   fSPEC_LIST x1 ++
 
1744
   fNODE "right" 1
 
1745
| CT_ring(x1) ->
 
1746
   fFORMULA_LIST x1 ++
 
1747
   fNODE "ring" 1
 
1748
| CT_simple_user_tac(x1, x2) ->
 
1749
   fID x1 ++
 
1750
   fTACTIC_ARG_LIST x2 ++
 
1751
   fNODE "simple_user_tac" 2
 
1752
| CT_simplify_eq(x1) ->
 
1753
   fID_OR_INT_OPT x1 ++
 
1754
   fNODE "simplify_eq" 1
 
1755
| CT_specialize(x1, x2, x3) ->
 
1756
   fINT_OPT x1 ++
 
1757
   fFORMULA x2 ++
 
1758
   fSPEC_LIST x3 ++
 
1759
   fNODE "specialize" 3
 
1760
| CT_split(x1) ->
 
1761
   fSPEC_LIST x1 ++
 
1762
   fNODE "split" 1
 
1763
| CT_subst(x1) ->
 
1764
   fID_LIST x1 ++
 
1765
   fNODE "subst" 1
 
1766
| CT_superauto(x1, x2, x3, x4) ->
 
1767
   fINT_OPT x1 ++
 
1768
   fID_LIST x2 ++
 
1769
   fDESTRUCTING x3 ++
 
1770
   fUSINGTDB x4 ++
 
1771
   fNODE "superauto" 4
 
1772
| CT_symmetry(x1) ->
 
1773
   fCLAUSE x1 ++
 
1774
   fNODE "symmetry" 1
 
1775
| CT_tac_double(x1, x2) ->
 
1776
   fID_OR_INT x1 ++
 
1777
   fID_OR_INT x2 ++
 
1778
   fNODE "tac_double" 2
 
1779
| CT_tacsolve(x,l) ->
 
1780
   fTACTIC_COM x ++
 
1781
   (List.fold_left (++) (mt()) (List.map fTACTIC_COM l)) ++
 
1782
   fNODE "tacsolve" (1 + (List.length l))
 
1783
| CT_tactic_fun(x1, x2) ->
 
1784
   fID_OPT_NE_LIST x1 ++
 
1785
   fTACTIC_COM x2 ++
 
1786
   fNODE "tactic_fun" 2
 
1787
| CT_then(x,l) ->
 
1788
   fTACTIC_COM x ++
 
1789
   (List.fold_left (++) (mt()) (List.map fTACTIC_COM l)) ++
 
1790
   fNODE "then" (1 + (List.length l))
 
1791
| CT_transitivity(x1) ->
 
1792
   fFORMULA x1 ++
 
1793
   fNODE "transitivity" 1
 
1794
| CT_trivial -> fNODE "trivial" 0
 
1795
| CT_trivial_with(x1) ->
 
1796
   fID_NE_LIST_OR_STAR x1 ++
 
1797
   fNODE "trivial_with" 1
 
1798
| CT_truecut(x1, x2) ->
 
1799
   fID_OPT x1 ++
 
1800
   fFORMULA x2 ++
 
1801
   fNODE "truecut" 2
 
1802
| CT_try(x1) ->
 
1803
   fTACTIC_COM x1 ++
 
1804
   fNODE "try" 1
 
1805
| CT_use(x1) ->
 
1806
   fFORMULA x1 ++
 
1807
   fNODE "use" 1
 
1808
| CT_use_inversion(x1, x2, x3) ->
 
1809
   fID_OR_INT x1 ++
 
1810
   fFORMULA x2 ++
 
1811
   fID_LIST x3 ++
 
1812
   fNODE "use_inversion" 3
 
1813
| CT_user_tac(x1, x2) ->
 
1814
   fID x1 ++
 
1815
   fTARG_LIST x2 ++
 
1816
   fNODE "user_tac" 2
 
1817
and fTACTIC_OPT = function
 
1818
| CT_coerce_NONE_to_TACTIC_OPT x -> fNONE x
 
1819
| CT_coerce_TACTIC_COM_to_TACTIC_OPT x -> fTACTIC_COM x
 
1820
and fTAC_DEF = function
 
1821
| CT_tac_def(x1, x2) ->
 
1822
   fID x1 ++
 
1823
   fTACTIC_COM x2 ++
 
1824
   fNODE "tac_def" 2
 
1825
and fTAC_DEF_NE_LIST = function
 
1826
| CT_tac_def_ne_list(x,l) ->
 
1827
   fTAC_DEF x ++
 
1828
   (List.fold_left (++) (mt()) (List.map fTAC_DEF l)) ++
 
1829
   fNODE "tac_def_ne_list" (1 + (List.length l))
 
1830
and fTARG = function
 
1831
| CT_coerce_BINDING_to_TARG x -> fBINDING x
 
1832
| CT_coerce_COFIXTAC_to_TARG x -> fCOFIXTAC x
 
1833
| CT_coerce_FIXTAC_to_TARG x -> fFIXTAC x
 
1834
| CT_coerce_FORMULA_OR_INT_to_TARG x -> fFORMULA_OR_INT x
 
1835
| CT_coerce_PATTERN_to_TARG x -> fPATTERN x
 
1836
| CT_coerce_SCOMMENT_CONTENT_to_TARG x -> fSCOMMENT_CONTENT x
 
1837
| CT_coerce_SIGNED_INT_LIST_to_TARG x -> fSIGNED_INT_LIST x
 
1838
| CT_coerce_SINGLE_OPTION_VALUE_to_TARG x -> fSINGLE_OPTION_VALUE x
 
1839
| CT_coerce_SPEC_LIST_to_TARG x -> fSPEC_LIST x
 
1840
| CT_coerce_TACTIC_COM_to_TARG x -> fTACTIC_COM x
 
1841
| CT_coerce_TARG_LIST_to_TARG x -> fTARG_LIST x
 
1842
| CT_coerce_UNFOLD_to_TARG x -> fUNFOLD x
 
1843
| CT_coerce_UNFOLD_NE_LIST_to_TARG x -> fUNFOLD_NE_LIST x
 
1844
and fTARG_LIST = function
 
1845
| CT_targ_list l ->
 
1846
   (List.fold_left (++) (mt()) (List.map fTARG l)) ++
 
1847
   fNODE "targ_list" (List.length l)
 
1848
and fTERM_CHANGE = function
 
1849
| CT_check_term(x1) ->
 
1850
   fFORMULA x1 ++
 
1851
   fNODE "check_term" 1
 
1852
| CT_inst_term(x1, x2) ->
 
1853
   fID x1 ++
 
1854
   fFORMULA x2 ++
 
1855
   fNODE "inst_term" 2
 
1856
and fTEXT = function
 
1857
| CT_coerce_ID_to_TEXT x -> fID x
 
1858
| CT_text_formula(x1) ->
 
1859
   fFORMULA x1 ++
 
1860
   fNODE "text_formula" 1
 
1861
| CT_text_h l ->
 
1862
   (List.fold_left (++) (mt()) (List.map fTEXT l)) ++
 
1863
   fNODE "text_h" (List.length l)
 
1864
| CT_text_hv l ->
 
1865
   (List.fold_left (++) (mt()) (List.map fTEXT l)) ++
 
1866
   fNODE "text_hv" (List.length l)
 
1867
| CT_text_op l ->
 
1868
   (List.fold_left (++) (mt()) (List.map fTEXT l)) ++
 
1869
   fNODE "text_op" (List.length l)
 
1870
| CT_text_path(x1) ->
 
1871
   fSIGNED_INT_LIST x1 ++
 
1872
   fNODE "text_path" 1
 
1873
| CT_text_v l ->
 
1874
   (List.fold_left (++) (mt()) (List.map fTEXT l)) ++
 
1875
   fNODE "text_v" (List.length l)
 
1876
and fTHEOREM_GOAL = function
 
1877
| CT_goal(x1) ->
 
1878
   fFORMULA x1 ++
 
1879
   fNODE "goal" 1
 
1880
| CT_theorem_goal(x1, x2, x3, x4) ->
 
1881
   fDEFN_OR_THM x1 ++
 
1882
   fID x2 ++
 
1883
   fBINDER_LIST x3 ++
 
1884
   fFORMULA x4 ++
 
1885
   fNODE "theorem_goal" 4
 
1886
and fTHM = function
 
1887
| CT_thm x -> fATOM "thm" ++
 
1888
   (f_atom_string x) ++
 
1889
   str "\n"
 
1890
and fTHM_OPT = function
 
1891
| CT_coerce_NONE_to_THM_OPT x -> fNONE x
 
1892
| CT_coerce_THM_to_THM_OPT x -> fTHM x
 
1893
and fTYPED_FORMULA = function
 
1894
| CT_typed_formula(x1, x2) ->
 
1895
   fFORMULA x1 ++
 
1896
   fFORMULA x2 ++
 
1897
   fNODE "typed_formula" 2
 
1898
and fUNFOLD = function
 
1899
| CT_coerce_ID_to_UNFOLD x -> fID x
 
1900
| CT_unfold_occ(x1, x2) ->
 
1901
   fID x1 ++
 
1902
   fINT_NE_LIST x2 ++
 
1903
   fNODE "unfold_occ" 2
 
1904
and fUNFOLD_NE_LIST = function
 
1905
| CT_unfold_ne_list(x,l) ->
 
1906
   fUNFOLD x ++
 
1907
   (List.fold_left (++) (mt()) (List.map fUNFOLD l)) ++
 
1908
   fNODE "unfold_ne_list" (1 + (List.length l))
 
1909
and fUSING = function
 
1910
| CT_coerce_NONE_to_USING x -> fNONE x
 
1911
| CT_using(x1, x2) ->
 
1912
   fFORMULA x1 ++
 
1913
   fSPEC_LIST x2 ++
 
1914
   fNODE "using" 2
 
1915
and fUSINGTDB = function
 
1916
| CT_coerce_NONE_to_USINGTDB x -> fNONE x
 
1917
| CT_usingtdb -> fNODE "usingtdb" 0
 
1918
and fVAR = function
 
1919
| CT_var x -> fATOM "var" ++
 
1920
   (f_atom_string x) ++
 
1921
   str "\n"
 
1922
and fVARG = function
 
1923
| CT_coerce_AST_to_VARG x -> fAST x
 
1924
| CT_coerce_AST_LIST_to_VARG x -> fAST_LIST x
 
1925
| CT_coerce_BINDER_to_VARG x -> fBINDER x
 
1926
| CT_coerce_BINDER_LIST_to_VARG x -> fBINDER_LIST x
 
1927
| CT_coerce_BINDER_NE_LIST_to_VARG x -> fBINDER_NE_LIST x
 
1928
| CT_coerce_FORMULA_LIST_to_VARG x -> fFORMULA_LIST x
 
1929
| CT_coerce_FORMULA_OPT_to_VARG x -> fFORMULA_OPT x
 
1930
| CT_coerce_FORMULA_OR_INT_to_VARG x -> fFORMULA_OR_INT x
 
1931
| CT_coerce_ID_OPT_OR_ALL_to_VARG x -> fID_OPT_OR_ALL x
 
1932
| CT_coerce_ID_OR_INT_OPT_to_VARG x -> fID_OR_INT_OPT x
 
1933
| CT_coerce_INT_LIST_to_VARG x -> fINT_LIST x
 
1934
| CT_coerce_SCOMMENT_CONTENT_to_VARG x -> fSCOMMENT_CONTENT x
 
1935
| CT_coerce_STRING_OPT_to_VARG x -> fSTRING_OPT x
 
1936
| CT_coerce_TACTIC_OPT_to_VARG x -> fTACTIC_OPT x
 
1937
| CT_coerce_VARG_LIST_to_VARG x -> fVARG_LIST x
 
1938
and fVARG_LIST = function
 
1939
| CT_varg_list l ->
 
1940
   (List.fold_left (++) (mt()) (List.map fVARG l)) ++
 
1941
   fNODE "varg_list" (List.length l)
 
1942
and fVERBOSE_OPT = function
 
1943
| CT_coerce_NONE_to_VERBOSE_OPT x -> fNONE x
 
1944
| CT_verbose -> fNODE "verbose" 0
 
1945
;;