Global Index

||, 9.2
*, 3.1.3, 3.2.2
+, 3.1.3, 3.2.2
-, 3.2.2
/, 3.2.2
2-level approach, 8.10.3
;, 9.2
;[...|...|...], 9.2
<, 3.2.2
<=, 3.2.2
>, 3.2.2
>=, 3.2.2
?, 8.2.2
?=, 3.2.2
%, 11.2.2
&, 3.1.4
_, 1.2.11
{A}+{B}, 3.1.4
{x:A & (P x)}, 3.1.4
{x:A | (P x)}, 3.1.4
|, 3.1.4
A*B, 3.1.3
A+{B}, 3.1.4
A+B, 3.1.3
Abbreviations, 11.3
Abort, 7.1.6
About, 2
Absolute names, 2.5.2
Acc, 3.1.6
Acc_inv, 3.1.6
Acc_rec, 3.1.6
Add Abstract Ring, 2
Add Abstract Semi Ring, 3
Add Field, 8.11.10
Add LoadPath, 6.5.3
Add ML Path, 6.5.7
Add Morphism, 20.3
Add Printing If ident, 2.2.4
Add Printing Let ident, 2.2.4
Add Rec LoadPath, 6.5.4
Add Rec ML Path, 6.5.8
Add Ring, 8.11.8, 19.5
Add Semi Ring, 1
Add Semi Ring, 8.11.8
Add Setoid, 20.2
Admitted, 1.3.5, 7.1.3
Arguments Scope, 11.2.2
Arithmetical notations, 3.2.2
Arity, 4.5.3
Associativity, 11.1.2
Axiom, 1.3.1
Axiom (and coercions), 5
abstract, 9.2
abstractions, 1.2.7
absurd, 3.1.2, 8.4.1
absurd_set, 3.1.4
all, 3.1.2
and, 3.1.2
and_rec, 3.1.4
app, 3.2.5
applications, 1.2.9
apply, 8.3.6
apply ... with, 1
assert, 8.3.8
assumption, 8.3.1
auto, 8.11.1
autorewrite, 8.11.12
Back, 6.6.2
Bad Magic Number, 3
Begin Silent, 6.8.1
Bind Scope, 11.2.2
Binding list, 8.3.11
BNF metasyntax, 1
beta-reduction, 4.3, 4.3
binders, 1.2.6
bool, 3.1.3
bool_choice, 3.1.4
byte-code, 12.1
Calculus of (Co)Inductive Constructions, 4
Calculus of (Co)Inductive Constructions, 4
Canonical Structure, 2.6.10
Cases, 15
Cast, 1.2.10
Cd, 6.5.2
Check, 6.2.1
Choice, 3.1.4
Choice2, 3.1.4
CIC, 4
Clauses, 8.5
Close Scope, 11.2.1
Coercion, 2.7, 16.6.1, 2
Coercion Local, 1, 4
Coercions, 2.7
- and records, 16.9
- and sections, 16.10
- classes, 16.2
- Funclass, 16.3
- identity, 16.4
- inheritance graph, 16.5
- presentation, 16
- Sortclass, 16.3
CoFixpoint, 1.3.4
CoFixpoint ... where ..., 11.1.8
CoInductive, 1.3.3
CoInductive (and coercions), 6
Comments, 1.1
Compiled files, 6.4
Conjecture, 1.3.1
Connectives, 3.1.2
Constant, 1.3.2
Context, 4.2
Contributions, 3.3
Conversion rules, 4.3
Conversion tactics, 8.5
coqdep, 13.2
coqdoc, 13.4
coq_Makefile, 13.3
coqmktop, 13.1
coq-tex, 13.6
case, 4
case ... with, 5
cbv, 8.5.1
change, 8.3.10
change ... in, 8.3.10
clear, 8.3.2
clearbody, 2
compare, 8.9.2
compute, 8.5.1, 1
congruence, 8.11.6
conj, 3.1.2
constructor, 8.6.1
constructor ... with, 2
context
- in expression, 9.2
- in pattern, 9.2
contradiction, 8.4.2
coqc, 12
coqide, 14
coqtop, 12
cut, 3
cutrewrite, 8.8.2
Datatypes, 3.1.3
Debugger, 13.1
Declarations, 1.3.1
Declare Left Step, 8.8.8
Declare ML Module, 6.4.3
Declare Right Step, 8.8.8
Defined, 1.3.5, 1
Definition, 1.3.2, 3
Definitions, 1.3.2
Delimit Scope, 11.2.2
Dependencies, 13.2
Derive Dependent Inversion, 2
Derive Dependent Inversion_clear, 3
Derive Inversion, 8.10.2
Derive Inversion_clear, 1
Derive Inversion_clear ... with, 1
Drop, 6.7.2
decide equality, 8.9.1
decompose, 8.7.5
decompose record, 2
decompose sum, 1
delta-reduction, 1.3.2, 4.3, 4.3
dependent inversion, 10
dependent inversion ... as , 11
dependent inversion ... as ... with, 15
dependent inversion ... with, 14
dependent inversion_clear, 12
dependent inversion_clear ... as, 13
dependent inversion_clear ... as ... with, 17
dependent inversion_clear ... with, 16
dependent rewrite ->, 8.9.6
dependent rewrite <-, 1
destruct, 8.7.2
discriminate, 8.9.3, 2
discrR, 3.2.4
do, 9.2
double induction, 8.7.4
Elimination
- Empty elimination, 4.5.4
- Singleton elimination, 4.5.4
Elimination sorts, 4.5.4
Emacs, 13.7
End, 2.3.2, 2.4.2, 2.4.5
End Silent, 6.8.2
Environment, 1.3.2, 4.2
Environment variables, 12.4
Equality, 3.1.2
Eval, 6.2.2
Exc, 3.1.4
Except, 3.1.4
Explicitation of implicit arguments, 2.6.7
Export, 1
Extract Constant, 18.2.3
Extract Inductive, 18.2.3
Extraction, 18
Extraction, 6.2.3, 18.1
Extraction Inline, 18.2.2
Extraction Language, 18.2.1
Extraction Module, 18.1
Extraction NoInline, 18.2.2
eapply, 3, 10.2
eauto, 8.11.2
elim ... using, 8
elim ... with, 6
elimtype, 9
eq, 3.1.2
eq_add_S, 3.1.5
eq_ind_r, 3.1.2
eq_rec, 3.1.4
eq_rec_r, 3.1.2
eq_rect, 3.1.2
eq_rect_r, 3.1.2
eq_S, 3.1.5
error, 3.1.4
eta-conversion, 4.3
eta-reduction, 4.3
eval
- in Ltac, 9.2
ex, 3.1.2
ex2, 3.1.2
ex_intro, 3.1.2
ex_intro2, 3.1.2
exact, 8.2.1
exist, 3.1.4
exist2, 3.1.4
existS, 3.1.4
existS2, 3.1.4
exists, 3.1.2, 4
exists2, 3.1.2
Fact, 1.3.5, 2
False, 3.1.2
False_rec, 3.1.4
Fix, 4.5.5
Fix_F, 3.1.6
Fix_F_eq, 3.1.6
Fix_F_inv, 3.1.6
Fixpoint, 1.3.4
Fixpoint ... where ..., 11.1.8
Focus, 7.2.5
Functional Scheme, 8.14, 10.4
f_equal, 3.1.2
f_equali, 3.1.2
fail, 9.2
false, 3.1.3
field, 8.11.9
first, 9.2
firstorder, 8.11.5
firstorder tactic, 1
firstorder using, 3
firstorder with, 2
fix ident_i{...}, 1.2.14
fix_eq, 3.1.6
flat_map, 3.2.5
fold, 8.5.6
fold_left, 3.2.5
fold_right, 3.2.5
form, 1.2.5
fourier, 8.11.11
fresh
- in Ltac, 9.2
fst, 3.1.3
fun
- in Ltac, 9.2
functional induction, 8.7.6, 10.4
Gallina, 1, 2
gallina, 13.8
Goal, 1.3.5, 7.1.1
ge, 3.1.5
generalize, 8.3.9
generalize dependent, 2
goal, 8
gt, 3.1.5
Head normal form, 4.3
Hint, 8.12
Hint Constructors, 8.12
Hint Extern, 8.12
Hint Immediate, 8.12
Hint Resolve, 8.12
Hint Rewrite, 8.11.13
Hint Unfold, 8.12
Hints databases, 8.12
Hypotheses, 1.3.1
Hypothesis, 1.3.1
Hypothesis (and coercions), 5
head, 3.2.5
hnf, 8.5.3
I, 3.1.2
Identity Coercion, 16.6.2
IF_then_else, 3.1.2
Implicit Arguments, 2.6.2
Implicit arguments, 2.6
Import, 2.4.10
Inductive, 1.3.3
Inductive (and coercions), 6
Inductive ... where ..., 11.1.8
Inductive definitions, 1.3.3
Infix, 11.1.6
Inspect, 1
Interpretation scopes, 11.2
IsSucc, 3.1.5
ident, 1.1
identity, 3.1.3
idtac, 9.2
if ... then ... else, 2.2.2
iff, 3.1.2
induction, 8.7.1
info, 9.2
injection, 8.9.4, 2
inl, 3.1.3
inleft, 3.1.4
inr, 3.1.3
inright, 3.1.4
integer, 1.1
intro, 8.3.5
intro ... after, 7
intro after, 6
intros, 1
intros intro_pattern, 8.7.3
intros until, 4, 5
intuition, 8.11.4
inversion, 8.10.1, 10.5
inversion ... as, 3
inversion ... as ... in, 7
inversion ... in, 6
inversion ... using, 20
inversion ... using ... in, 21
inversion_clear, 2
inversion_clear ... as ... in, 9
inversion_clear ... in, 8
inversion_cleardots as, 5
iota-reduction, 4.3, 4.3, 4.5.4, 4.5.5
L^AT_EX, 13.6
Lemma, 1.3.5, 1
Let, 1.3.2
Lexical conventions, 1.1
Libraries, 2.5.1
Load, 6.3.1

Load Verbose, 2
Loadpath, 6.5
Local, 4
Local definitions, 1.2.12
Locate, 6.2.10, 11.1.10
Locate File, 6.5.10
Locate Library, 6.5.11
Logical paths, 2.5.1
Ltac
- eval, 9.2
- fresh, 9.2
- fun, 9.2
- let, 9.2
- let rec, 9.2
- match, 9.2
- match goal, 9.2
- match reverse goal, 9.2
- type of, 9.2
Ltac, 9.3
lambda-calculus, 5
lapply, 4
lazy, 8.5.1
le, 3.1.5
le_n, 3.1.5
le_S, 3.1.5
left, 3.1.4, 5
length, 3.2.5
let
- in Ltac, 9.2
let ... in, 2.2.3
let rec
- in Ltac, 9.2
let-in, 1.2.12
local context, 7
lt, 3.1.5
Makefile, 13.3
Man pages, 13.9
ML-like patterns, 2.2.1, 15
Module, 2.4.1, 2.4.3
Module Type, 2.4.4
Modules, 2.4
Mutual Inductive, 1.3.3
map, 3.2.5
match
- in Ltac, 9.2
match...with...end, 1.2.13, 2.2, 4.5.4
match goal
- in Ltac, 9.2
match reverse goal
- in Ltac, 9.2
mod, 3.2.2
move, 8.3.3
mult, 3.1.5
mult_n_O, 3.1.5
mult_n_Sm, 3.1.5
None, 3.1.3
Normal form, 4.3
Notation, 11.1, 11.3
Notations for lists, 3.2.5
Notations for real numbers, 3.2.4
n_Sn, 3.1.5
nat, 3.1.3
nat_case, 3.1.5
nat_double_ind, 3.1.5
nat_scope, 3.2.3
native code, 12.1
not, 3.1.2
not_eq_S, 3.1.5
notT, 3.1.7
nth, 3.2.5
num, 1.1
O, 3.1.3
O_S, 3.1.5
Opaque, 6.2.4
Open Scope, 11.2.1
Options of the command line, 12.5
omega, 8.11.7, 17.1
option, 3.1.3
or, 3.1.2
or_introl, 3.1.2
or_intror, 3.1.2
Parameter, 1.3.1
Parameter (and coercions), 5
Parameters, 1.3.1
Peano's arithmetic, 3.2.3
Positivity, 4.5.3
Precedences, 11.1.2
Predicative Calculus of (Co)Inductive Constructions, 4
Print, 6.1.1
Print All, 6.1.2
Print Classes, 16.7.1
Print Coercion Paths, 16.7.4
Print Coercions, 16.7.2
Print Extraction Inline, 18.2.2
Print Grammar constr, 11.1.4
Print Graph, 16.7.3
Print Hint, 8.12.2
Print HintDb, 3
Print Implicit, 2.6.8
Print LoadPath, 6.5.6
Print ML Modules, 6.4.4
Print ML Path, 6.5.9
Print Module, 2.4.11
Print Module Type, 2.4.12
Print Modules, 6.4.2
Print Section, 2
Print Table Printing If, 2.2.4
Print Table Printing Let, 2.2.4
Print Term, 1
Print XML, 13.5.5
Programming, 3.1.3
Prompt, 7
Proof, 1.3.5, 7.1.5
Proof editing, 7
Proof General, 13.7.2
Proof rendering, 13.5
Proof term, 7
Prop, 1.2.5, 4.1.1
Pwd, 6.5.1
pair, 3.1.3
pairT, 3.1.7
pattern, 8.5.7
pCIC, 4
plus, 3.1.5
plus_n_O, 3.1.5
plus_n_Sm, 3.1.5
pose, 8.3.7
pred, 3.1.5
pred_Sn, 3.1.5
prod, 3.1.3
prodT, 3.1.7
products, 1.2.8
progress, 9.2
proj1, 3.1.2
proj2, 3.1.2
projS1, 3.1.4
projS2, 3.1.4
Qed, 1.3.5, 7.1.2
Qualified identifiers, 2.5.2
Quantifiers, 3.1.2
Quit, 6.7.1
qualid, 2.6.7
quote, 8.10.3, 10.7
Record, 2.1
Recursion, 3.1.6
Recursive arguments, 4.5.5
Recursive Extraction, 18.1
Recursive Extraction Module, 18.1
Remark, 1.3.5, 2
Remove LoadPath, 6.5.5
Remove Printing If ident, 2.2.4
Remove Printing Let ident, 2.2.4
Require, 6.4.1
Require Export, 1
ReservedNotation, 11.1.7
Reset, 6.6.1
Reset Extraction Inline, 18.2.2
Reset Initial, 2
Resource file, 12.3
Restart, 7.2.4
Restore State, 6.6.3
Resume, 7.1.8
red, 8.5.2
refine, 8.2.2, 10.1
refl_equal, 3.1.2
refl_identity, 3.1.3
reflexivity, 8.8.4
rename, 8.3.4
repeat, 9.2
replace ... with, 8.8.3
rev, 3.2.5
rewrite, 8.8.1
rewrite ->, 1
rewrite -> ... in, 4
rewrite <-, 2
rewrite <- ... in, 5
rewrite ... in, 3
right, 3.1.4, 5
ring, 8.11.8, 19, 19.4
S, 3.1.3
Save, 1.3.5, 2
Scheme, 8.13, 10.3
Script file, 6.3
Search, 6.2.6
SearchAbout, 6.2.7
SearchPattern, 6.2.8
SearchPattern ... inside ..., 1
SearchPattern ... outside ..., 2
SearchRewrite, 6.2.9
Section, 2.3.1
Sections, 2.3
Set, 1.2.5, 4.1.1
Set Contextual Implicit, 2.6.6
Set Extraction AutoInline, 18.2.2
Set Extraction Optimize, 18.2.2
Set Firstorder Depth, 8.11.5
Set Hyps Limit, 7.3.2
Set Implicit Arguments, 2.6.4
Set Printing All, 2.8
Set Printing Coercion, 16.8.2
Set Printing Coercions, 16.8.1
Set Printing Depth, 6.8.6
Set Printing Implicit, 2.6.9
Set Printing Notations, 11.1.9
Set Printing Synth, 2.2.4
Set Printing Width, 6.8.3
Set Printing Wildcard, 2.2.4
Set Strict Implicit, 2.6.5
Set Undo, 7.2.2
Show, 7.3.1
Show Conjectures, 7
Show Implicits, 2
Show Intro, 8
Show Intros, 9
Show Proof, 6
Show Script, 4
Show Tree, 5
Show XML Proof, 13.5.5
Silent mode, 6.8.1
Some, 3.1.3
Sorts, 1.2.5, 1.2.5, 4.1.1
Structure, 16.9
SubClass, 2
Substitution, 4.1.3
Suspend, 7.1.7
Syntactic Definition, 11.3
set, 8.3.7
setoid_replace, 20, 20.4
setoid_rewrite, 20.4
sig, 3.1.4
sig2, 3.1.4
sigS, 3.1.4
sigS2, 3.1.4
simpl, 8.5.4
simpl ... in, 8.5.4
simple destruct, 6
simple induction, 10
simple inversion, 18
simple inversion ... as, 19
simplify_eq, 8.9.5
snd, 3.1.3
solve, 9.2
sort, 1.1
specif, 1.2.5
split, 3
split_Rabs, 3.2.4
split_Rmult, 3.2.4
stepl, 8.8.8
stepr, 8.8.8
string, 1.1
subgoal, 8
subst, 8.8.7
sum, 3.1.3
sumbool, 3.1.4
sumor, 3.1.4
sym_eq, 3.1.2
sym_not_eq, 3.1.2
symmetry, 8.8.5
symmetry in, 8.8.5
Tactic Definition, 8.15
Tacticals, 9.2
- tactic₁;tactic₂, 9.2
- ; [ , ]9.2
- abstract, 9.2
- do, 9.2
- fail, 9.2
- first, 9.2
- idtac, 9.2
- info, 9.2
- ||, 9.2
- repeat, 9.2
- solve, 9.2
- try, 9.2
Tactics, 8
Terms, 1.2
Test Printing Depth, 6.8.8
Test Printing If ident, 2.2.4
Test Printing Let ident, 2.2.4
Test Printing Synth, 2.2.4
Test Printing Width, 6.8.5
Test Printing Wildcard, 2.2.4
Theorem, 1.3.5, 7.1.4
Theories, 3
Time, 6.7.3
Transparent, 6.2.5
True, 3.1.2
Type, 1.2.5, 4.1.1
Type of constructor, 4.5.3
Typing rules, 4.2, 8.3
- App, 4.2, 3
- Ax, 4.2
- Const, 4.2
- Conv, 4.3, 8.3.5, 8.3.10
- Fix, 4.5.5
- Lam, 4.2, 8.3.5
- Let, 4.2, 8.3.5
- match, 4.5.4
- Prod, 4.2
- Prod (impredicative Set), 4.7
- Var, 4.2, 8.3.1
tactic, 8.1
tactic macros, 8.15
tail, 3.2.5
tauto, 8.11.3
term, 1.1
trans_eq, 3.1.2
transitivity, 8.8.6
trivial, 4
true, 3.1.3
try, 9.2
tt, 3.1.3
type, 1.2.2, 1.2.6
type of
- in Ltac, 9.2
type_scope, 11.2.3
Undo, 7.2.1
Unfocus, 7.2.6
Unset Contextual Implicit, 2.6.6
Unset Extraction AutoInline, 18.2.2
Unset Extraction Optimize, 18.2.2
Unset Hyps Limit, 7.3.3
Unset Implicit Arguments, 2.6.4
Unset Printing All, 2.8
Unset Printing Coercion, 16.8.2
Unset Printing Coercions, 16.8.1
Unset Printing Depth, 6.8.7
Unset Printing Implicit, 2.6.9
Unset Printing Notations, 11.1.9
Unset Printing Synth, 2.2.4
Unset Printing Width, 6.8.4
Unset Printing Wildcard, 2.2.4
Unset Strict Implicit, 2.6.5
Unset Undo, 7.2.3
unfold, 8.5.5
unfold ... in, 1
unit, 3.1.3
Variable, 1.3.1
Variable (and coercions), 5
Variables, 1.3.1
value, 3.1.4
Well founded induction, 3.1.6
Well foundedness, 3.1.6
Write State, 6.6.4
well_founded, 3.1.6
XML exportation, 13.5
zeta-reduction, 4.3, 4.3