Global Index

• "| 137
• * 130
• + 125
• .vo files 286
• ; 491
• ;[... |... |...] 493
• ? 320
• A*B 129
• A+B 124
• A+{B} 157
• AST 508
• AST patterns 513
• Abort 347
• Abstract 499
• Abstract syntax tree 509
• Absurd 388
• Acc 194
• Acc_inv 195
• Acc_rec 196
• Add ML Path 305
• Add Natural 577
• Add Natural Contractible 582
• Add Natural Implicit 580 581
• Add Natural Transparent 583
• Add Printing If ident 61
• Add Printing Let ident 57
• Add Ring 471 603
• Add Semi Ring 472 604
• AddPath 302
• All 95
• AllT 199
• Apply 380
• Apply ...with 381
• Arithmetical notations 219
• Arity 253
• Assumption 373
• Auto 460
• Axiom 21
• Bad Magic Number 295
• Begin Silent 328
• Binding list 387
• Calculus of (Co)Inductive Constructions 223 224
• Case 415
• Case ...with 416
• Cases...of...end 19 47 255
• Cbv 394
• Cd 301
• Change 392
• Chapter 67
• Check 273
• Choice 158
• Choice2 159
• CIC 222
• Class 73 560
• Clear 375
• CoFixpoint 37
• CoInductive 35
• Coercion 74 561
• Coercions 72
  • FUNCLASS 556
  • SORTCLASS 557
  • and records 565
  • and sections 567
  • classes 555
  • identity 558
  • inheritance graph 559
  • presentation 554
• Comments 2
• Compare 435
• Compile Module 285
• Compile Module Specification 287
• Compile Verbose Module 288
• Compiled files 283
• Compute 396
• Connectives 79
• Constant 28
• Constructor 404
• Constructor ...with 405
• Context 231
• Contradiction 389
• Contributions 221
• Conversion rules 240
• Conversion tactics 390
• coq2html 548
• coq2latex 546
• Coq_SearchIsos 538
• coqdep 535
• coqmktop 532
• coq-tex 545
• Cut 384
• CutRewrite 429
• Datatypes 114
• Debugger 533
• Decide Equality 434
• Declarations 20
• Declare ML Module 297
• Decompose 420
• Decompose Record 422
• Decompose Sum 421
• Defined 340
• Definition 30 345
• Definitions 26
• DelPath 303
• Dependencies 534
• Dependent Inversion 448
• Dependent Inversion ...with 450
• Dependent Inversion_clear 449
• Dependent Inversion_clear ...with 451
• Dependent Rewrite -> 442
• Dependent Rewrite <- 443
• Derive Dependent Inversion 458
• Derive Dependent Inversion_clear 459
• Derive Inversion 455
• Derive Inversion_clear 456
• Derive Inversion_clear ...with 457
• Destruct 417
• Discriminate 436 437
• Do 486
• do_Makefile 537
• Double Induction 419
• Drop 327
• EApply 382 505
• EAuto 462
• ETrivial 463
• EX 98
• EXT 204
• Elim 410
• Elim ...using 412
• Elim ...with 411
• ElimType 413
• Elimination
  • Singleton elimination 259
• Elimination sorts 256
• Emacs 549
• EmptyT 208
• End 68
• End Silent 330
• Environment 29 232
• Equality 103
• Eval 274
• Ex 97
• Ex2 101
• ExT 203
• ExT2 206
• Exact 369
• Exc 161
• Except 166
• Exists 407
• Extendable Grammars 514
• Extensive grammars 324
• Extraction 275
• Fact 344
• Fail 484
• False 82
• False_rec 164
• Fix 262
• Fixpoint 36
• Focus 354
• Fold 402
• Fst 134
• #GENTERM 525
• Gallina 0 45
• Generalize 386
• Goal 44 337
• Grammar 323 515
• Grammar Actions 518
• Grammar entries 517
• HTML 547
• Head normal form 251
• Hint 477
• Hint Unfold 479
• Hints list 476
• Hnf 398
• Hypothesis 25
• I 81
• IF 92
• Idtac 482
• Immediate 478
• Implicit Arguments 69
• Implicit Arguments Off 318
• Implicit Arguments On 317
• Import 290
• Induction 414
• Inductive 33
• Inductive definitions 32
• Infix 325
• Info 497
• Injection 439 440
• Inspect 270
• Intro 376
• Intros 378 418
• Intros until 379
• Intuition 466
• Inversion 444 507
• Inversion ...in 446
• Inversion ...using 452
• Inversion ...using ...in 453
• Inversion_clear 445
• Inversion_clear ...in 447
• IsSucc 174
• LApply 383
• LL(1) 521
• L^aT_eX 544
• Lazy 395
• Left 408
• Lemma 39 342
• Lexical conventions 1
• Linear 467
• Linear with 468
• Load 281
• Load Verbose 282
• Loadpath 299
• Local 31
• Locate 309
• Locate File 307
• Locate Library 308
• ML Import 573
• ML Inductive 572
• ML-like patterns 48 553
• Makefile 536
• Man pages 551
• Match ...with ...end 266
• Metavariable 510
• Modules 284
• Mutual Inductive 34
• Normal form 250
• O 121
• O_S 175
• Omega 469 585
• Opaque 276
• Options of the command line 531
• Orelse 488
• Parameter 22
• Pattern 403
• Peano's arithmetic notations 220
• Positivity 252
• Pretty printing 322
• Print 267 272
• Print All 269
• Print Classes 75 562
• Print Coercions 76 563
• Print Grammar 523
• Print Graph 77 564
• Print Hint 480
• Print LoadPath 304
• Print ML Modules 298
• Print ML Path 306
• Print Modules 296
• Print Natural 574
• Print Printing If 64
• Print Printing Let 60
• Print Printing Synth 56
• Print Printing Wildcard 53
• Print Proof 268
• Print Section 271
• Print States 312
• Program 474 597
• Program_Expand 599
• Program_all 475 598
• Programming 113
• Prolog 464
• Prompt 334
• Proof 40 41 346
• Proof editing 333
• Proof term 336
• Prop 11 227
• Pwd 300
• Qed 42 338
• Quantifiers 93
• Quit 326
• Quotations 512
• Quoted AST 511
• Read Module 289
• Realizer 473 595
• Record 46
• Recursion 192
• Recursive arguments 264
• Red 397
• Refine 370 504
• Reflexivity 431
• Remark 343
• Remove Natural 578
• Remove Printing If ident 62
• Remove Printing Let ident 58
• Remove State 315
• Replace ...with 430
• Require 291
• Require Export 292
• Require Implementation 293
• Require Specification 294
• Reset 310
• Reset Initial 314
• Resource file 530
• Restart 353
• Restore State 313
• Resume 349
• Rewrite 423
• Rewrite -> 424
• Rewrite -> ...in 427
• Rewrite <- 425
• Rewrite <- ...in 428
• Rewrite ...in 426
• Right 409
• Ring 470 601 602
• S 122
• SELF 522
• Save 43 339
• Save State 311
• Scheme 501 506
• Script file 280
• Search 278
• SearchIsos 279
• Section 66
• Sections 65
• Set 10 228
• Set Hyps_limit 362
• Set Natural 575
• Set Natural Depth 584
• Set Omega Action 592
• Set Omega System 589
• Set Omega Time 586
• Set Printing Synth 54
• Set Printing Wildcard 51
• Set Undo 351
• Show 356
• Show Conjectures 361
• Show Implicits 357
• Show Natural 576
• Show Program 596
• Show Proof 360
• Show Script 358
• Show Tree 359
• Silent mode 329
• Simpl 399
• Simple Discriminate 438
• Simple Inversion 454
• Simplify_eq 441
• Small inductive type 257
• Snd 135
• Sorts 8 12 225
• Split 406
• Strong elimination 258
• Structure 566
• Substitution 230
• Suspend 348
• Switch Omega Action 594
• Switch Omega System 591
• Switch Omega Time 588
• Symmetry 432
• Syntactic Definition 70 319
• Syntax 321 524
• Tactic Definition 503
• Tacticals 481
  • Abstract 500
  • Do 487
  • Fail 485
  • Idtac 483
  • Info 498
  • Orelse 489
  • Repeat 490
  • Try 496
  • tactic₁;tactic₂ 492
  • tactic₀;[tactic₁ |... |tactic_n] 494
• Tactics 364
• Tauto 465
• Terms 5
• Test Natural 579
• Test Printing If ident 63
• Test Printing Let ident 59
• Theorem 38 341
• Theories 78
• Time 331
• Transitivity 433
• Transparent 277
• Trivial 461
• True 80
• Try 495
• Type 9 226
• Type of constructor 254
• Typing rules 233 372
  • App 239 385
  • Ax 234
  • Case 260
  • Const 236
  • Conv 247 391 393
  • Fix 263
  • Lam 238 377
  • Prod 237
  • Var 235 374
• UnSet Omega Action 593
• UnSet Omega System 590
• UnSet Omega Time 587
• Undo 350
• Unfocus 355
• Unfold 400
• Unfold ...in 401
• UnitT 209
• Unset Hyps_limit 363
• Unset Printing Synth 55
• Unset Printing Wildcard 52
• Unset Undo 352
• Untime 332
• Variable 23
• Variables 24
• Well founded induction 193
• Well foundedness 191
• Write Caml File 569
• Write CamlLight File 570
• Write Haskell File 571
• Write States 316
• & 143
• {A}+{B} 153
• {x:A "| (P x)} 136
• {x:A &(P x)} 142
• abstractions 16
• absurd 106
• absurd_set 167
• all 94
• allT 198
• and 84
• and_rec 168
• applications 18
• atomic tactics 367
• b-conversion 244
• b-reduction 241
• bool 117
• bool_choice 160
• byte-code 528
• case 520
• congr_eqT 216
• conj 85
• coqc 527
• coqtop 526
• coqtop -searchisos 540
• d-conversion 246
• d-reduction 27 243
• eq 104
• eqT 211
• eqT_ind_r 217
• eqT_rec_r 218
• eq_S 169
• eq_add_S 172
• eq_ind_r 111
• eq_rec 165
• eq_rec_r 112
• error 163
• h-conversion 248
• h-reduction 249
• ex 96
• ex2 100
• exT 202
• exT2 207
• exT_intro 205
• ex_intro 99
• ex_intro2 102
• exist 139
• exist2 141
• existS 145
• existS2 149
• f_equal 109
• false 119
• form 13
• fst 132
• ge 187
• gen 201
• goal 365
• gt 188
• ident 3
• if ... then ... else 49
• iff 91
• inl 126
• inleft 155
• inr 127
• inright 156
• inst 200
• i-conversion 245
• i-reduction 242 261 265
• l-calculus 229
• le 183
• le_S 185
• le_n 184
• left 151
• let 519
• let ... in ... 50
• local context 335
• lt 186
• mult 180
• mult_n_O 181
• mult_n_Sm 182
• n_Sn 176
• nat 120
• nat_case 189
• nat_double_ind 190
• native code 529
• not 83
• notT 210
• not_eq_S 173
• num 4
• or 88
• or_introl 89
• or_intror 90
• pair 131
• plus 177
• plus_n_O 178
• plus_n_Sm 179
• pred 170
• pred_Sn 171
• prod 128
• products 17
• proj1 86
• proj2 87
• projS1 146
• projS2 147
• ? 71
• rec 600
• refl_eqT 212
• refl_equal 105
• right 152
• sig 138
• sig2 140
• sigS 144
• sigS2 148
• snd 133
• sort 7
• specif 14
• subgoal 366
• sum 123
• sum_eqT 213
• sumbool 150
• sumor 154
• sym_equal 107
• sym_not_eqT 214
• sym_not_equal 110
• tactic 368
• tactic macros 502
• term 6
• trans_eqT 215
• trans_equal 108
• true 118
• tt 116
• type 15
• unit 115
• value 162
• well_founded 197