Index

Symbols

"All" is a predefined collection containing all variables. It can't be redefined (error) 'via' and 'abstract' cannot be used together (error) * (term), [1] + (backtracking branching) (tactic) + (term), [1] - (term) ... : ... (type cast) ... <: ... ... <<: ... ... is not definitionally an identity function (warning) ::= :> (coercion) (substructure) < (term) <= (term) => (tactic) > (term) >= (term) ?= (term) [ … | … | … ] (dispatch) (tactic) [> … | … | … ] (dispatch) (tactic) `( ) `(! ) `[ ] `[! ] `{ } `{! } { (tactic) {A}+{B} (term) {x:A & P x} (term) {x:A | P x} (term) || (first tactic making progress) (tactic) } (tactic) ‘coercion_class’ must be a transparent constant (error) ‘ident’ already exists (error) ‘ident’ already exists. (Axiom) (error)

‘ident’ already exists. (Definition) (error) ‘ident’ already exists. (Theorem) (error) ‘ident’ cannot be defined (warning) ‘ident’ cannot be defined because it is informative and ‘ident’ is not (warning) ‘ident’ cannot be defined because the projection ‘ident’ was not defined (warning) ‘ident’ is already declared as a typeclass (warning) ‘ident’ is already used (error) ‘ident’ is both name of a Collection and Variable, Collection ‘ident’ takes precedence over Variable (warning) ‘ident’ is declared as a local axiom (warning) ‘ident’ is not a local definition (error) ‘ident’ is not an equality of Σ types (error) ‘ident’ is opaque (error) ‘ident’ is used in the conclusion (error) ‘ident’ is used in the hypothesis ‘ident’ (error) ‘ident’ was already a defined Variable, the name ‘ident’ will refer to Collection when executing "Proof using" command (warning) ‘qualid’ cannot be used as a hint (error) ‘qualid’ does not occur (error) ‘qualid’ does not respect the uniform inheritance condition (warning) ‘qualid’ is already a coercion (error) ‘qualid’ is bound to a notation that does not denote a reference (error) ‘qualid’ is not a function (error) ‘qualid’ is not a module (error) ‘qualid’ is not an inductive type (error) ‘qualid’ not a defined object (error) ‘qualid’ not declared (error) ‘qualid’ should go from Byte.byte or (list Byte.byte) to ‘type’ or (option ‘type’) (error) ‘qualid’ should go from Number.int to ‘type’ or (option ‘type’). Instead of Number.int, the types Number.uint or Z or PrimInt63.pos_neg_int63 or PrimFloat.float or Number.number could be used (you may need to require BinNums or Number or PrimInt63 or PrimFloat first) (error) ‘qualid’ should go from ‘type’ to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)) (error) ‘qualid’ should go from ‘type’ to Number.int or (option Number.int). Instead of Number.int, the types Number.uint or Z or PrimInt63.pos_neg_int63 or Number.number could be used (you may need to require BinNums or Number or PrimInt63 first) (error) ‘qualid’ was already mapped to ‘qualid’ and cannot be remapped to ‘qualid’ (error) ‘string’ cannot be interpreted as a known notation in ‘ident’ entry. Make sure that symbols are surrounded by spaces and that holes are explicitly denoted by "_" (error) ‘string’ cannot be interpreted as a known notation. Make sure that symbols are surrounded by spaces and that holes are explicitly denoted by "_" (error) ‘type’ is not an inductive type (error) ‘type’ was already mapped to ‘type’, mapping it also to ‘type’ might yield ill typed terms when using the notation (warning) … : … (goal selector) (tactic) … : … (ssreflect) (tactic)

_

_

A

A coercion will be introduced instead of an instance in future versions when using ':>' in 'Class' declarations. Replace ':>' with '::' (or use '#[global] Existing Instance field.' for compatibility with Coq < 8.17) (warning) A*B (term) A+B (term) A+{B} (term) Abort (command) About (command) abstract (ssreflect) (tactic) abstract (tactic) absurd (tactic) (term) absurd_set (term) Acc (term) Acc_inv (term) Acc_rect (term) Activation of abbreviations does not expect mentioning a grammar entry (warning) Activation of abbreviations does not expect mentioning a scope (warning) Add (command) Add Field (command) Add Morphism (command) Add Parametric Morphism (command) Add Parametric Relation (command) Add Parametric Setoid (command) Add Relation (command) Add Ring (command) Add Setoid (command) Add Zify (command) add_bottom (attribute) add_top (attribute) admit (tactic) Admit Obligations (command) Admitted (command)

all (term) Allow StrictProp (flag) and (term) and_rect (term) app (term) apply (ssreflect) (tactic), [1] apply (tactic) Argument at position ‘natural’ is mentioned more than once (error) Argument of match does not evaluate to a term (error) Argument ‘name’ is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ] (error) Arguments (command) Arguments given by name or position not supported in explicit mode (error) Arguments of ring_simplify do not have all the same type (error) Arguments of section variables such as ‘name’ may not be renamed (error) Arithmetical notations assert (tactic) assert_fails (tactic) assert_succeeds (tactic) assumption (tactic) Asymmetric Patterns (flag) Attempt to save an incomplete proof (error) Attributes (command) auto (tactic) Auto Template Polymorphism (flag) autoapply (tactic) Automatically declaring ‘ident’ as template polymorphic (warning) autorewrite (tactic) autounfold (tactic) autounfold_one (tactic) Axiom (command) Axioms (command)

B

Back (command) BackTo (command) Bad lemma for decidability of equality (error) Bad magic number (error) Bad occurrence number of ‘qualid’ (error) Bad relevance (warning) Bad ring structure (error) Bind Scope (command) bool (term) bool_choice (term)

Boolean Equality Schemes (flag) Bound on the ceiling function (theorem) Brackets do not support multi-goal selectors (error) btauto (tactic) bullet (- + *) (tactic) Bullet Behavior (option) by (tactic) bypass_check(guard) (attribute) bypass_check(positivity) (attribute) bypass_check(universes) (attribute)

C

Cannot build functional inversion principle (warning) Cannot change ‘ident’, it is used in conclusion (error) Cannot change ‘ident’, it is used in hypothesis ‘ident’ (error) Cannot coerce ‘qualid’ to an evaluable reference (error) Cannot define graph for ‘ident’ (warning) Cannot define principle(s) for ‘ident’ (warning) Cannot find a declared ring structure for equality ‘term’ (error) Cannot find a declared ring structure over ‘term’ (error) Cannot find a relation to rewrite (error) Cannot find any non-recursive equality over ‘ident’ (error) Cannot find induction information on ‘qualid’ (error) Cannot find inversion information for hypothesis ‘ident’ (error) Cannot find library foo in loadpath (error) Cannot find the source class of ‘qualid’ (error) Cannot find the target class (error) Cannot import local constant, it will be ignored (warning) Cannot infer a term for this placeholder. (Casual use of implicit arguments) (error) Cannot infer a term for this placeholder. (refine) (error) Cannot interpret in ‘scope_name’ because ‘qualid’ could not be found in the current environment (error) Cannot interpret this number as a value of type ‘type’ (error) Cannot interpret this string as a value of type ‘type’ (error) Cannot load ‘qualid’: no physical path bound to ‘dirpath’ (error) Cannot move ‘ident’ after ‘ident’: it depends on ‘ident’ (error) Cannot move ‘ident’ after ‘ident’: it occurs in the type of ‘ident’ (error) Cannot recognize a boolean equality (error) Cannot recognize a statement based on ‘reference’ (error) Cannot recognize ‘coercion_class’ as a source class of ‘qualid’ (error) Cannot turn [inductive|constructor] into an evaluable reference (error) Cannot use mutual definition with well-founded recursion or measure (error) canonical (attribute) Canonical Structure (command) Can’t find file ‘ident’ on loadpath (error) case (ssreflect) (tactic) case (tactic) Case Analysis Schemes (flag) Case split (theorem) case_eq (tactic) Casts are not supported in this pattern (error) cbn (tactic) cbv (tactic) Cd (command) change (tactic) change_no_check (tactic) Check (command) Choice (term) Choice2 (term) Class (command)

classical_left (tactic) classical_right (tactic) clear (tactic) clear dependent (tactic) clearbody (attribute) (tactic) Close Scope (command) Coercion (command) cofix (tactic) CoFixpoint (command) CoInductive (command) Collection (command) Combined Scheme (command) command Comments (command) compare (tactic) Compiled library ‘ident’.vo makes inconsistent assumptions over library ‘qualid’ (error) Compute (command) compute (tactic) Condition not satisfied (error) congr (tactic), [1] congruence (tactic) conj (term) Conjecture (command) Conjectures (command) Connectives constr_eq (tactic) constr_eq_nounivs (tactic) constr_eq_strict (tactic) Constraint (command) constructor (tactic) Context (command) context (tactic) Contextual Implicit (flag) contradict (tactic) contradiction (tactic) convert (tactic) coqdoc Coqtop Exit On Error (flag) Corollary (command) Create HintDb (command) Cumulative (attribute) Cumulativity Weak Constraints (flag) cut (tactic) cutrewrite (tactic) cycle (tactic)

D

Datatypes Debug (command) (option) Debug Auto (flag) debug auto (tactic) Debug Eauto (flag) debug eauto (tactic) Debug mode not available in the IDE (error) Debug Ssreflect (flag) Debug SsrMatching (flag) Debug Trivial (flag) debug trivial (tactic) Decidable Equality Schemes (flag) decide (tactic) decide equality (tactic) Declare Custom Entry (command) Declare Equivalent Keys (command) Declare Instance (command) Declare Left Step (command) Declare ML Module (command) Declare Module (command) Declare Morphism (command) Declare Reduction (command) Declare Right Step (command) Declare Scope (command) Declaring arbitrary terms as hints is fragile it is recommended to declare a toplevel constant instead (warning) decompose (tactic) decompose record (tactic) decompose sum (tactic) Default Goal Selector (option) Default Proof Mode (option) Default Proof Using (option) Default Timeout (option)

Defined (command) Definition (command) Definitional UIP (flag) Delimit Scope (command) dependent destruction (tactic) dependent generalize_eqs (tactic) dependent generalize_eqs_vars (tactic) dependent induction (tactic) dependent inversion (tactic) dependent inversion_clear (tactic) dependent rewrite (tactic) dependent simple inversion (tactic) deprecated (attribute) Derive (command) Derive Dependent Inversion (command) Derive Dependent Inversion_clear (command) Derive Inversion (command) Derive Inversion_clear (command) destauto (tactic) destruct (tactic) dfs eauto (tactic) Diffs (option) dintuition (tactic) Disable Notation (command) discriminate (tactic) discrR (tactic) do (ssreflect) (tactic) do (tactic) done (tactic) Drop (command) dtauto (tactic) Dump Arith (option) Duplicate clear of H. Use { }H instead of { H }H (warning) Dynlink error: execution of module initializers in the (error)

E

eapply (tactic) eassert (tactic) eassumption (tactic) easy (tactic) eauto (tactic) ecase (tactic) econstructor (tactic) edestruct (tactic) ediscriminate (tactic) eelim (tactic) eenough (tactic) eexact (tactic) eexists (tactic) einduction (tactic) einjection (tactic) eintros (tactic) Either there is a type incompatibility or the problem involves dependencies (error) eleft (tactic) elim (ssreflect) (tactic) elim (tactic) Elimination Schemes (flag) Enable Notation (command) End (command) End of quoted string not followed by a space in notation (error) enough (tactic) epose (tactic) epose proof (tactic) eq (term) eq_add_S (term) eq_ind_r (term) eq_rec_r (term) eq_rect (term), [1] eq_rect_r (term) eq_refl (term) eq_S (term) eq_sym (term) eq_trans (term) Equality eremember (tactic) erewrite (tactic) eright (tactic) error (term) eset (tactic) esimplify_eq (tactic) esplit (tactic) etransitivity (tactic)

Eval (command) eval (tactic) evar (tactic) ex (term) ex2 (term) ex_intro (term) ex_intro2 (term) exact (ssreflect) (tactic) exact (tactic) exact_no_check (tactic) exactly_once (tactic) Example (command) Exc (term) exfalso (tactic) exist (term) exist2 (term) Existing Class (command) Existing Instance (command) Existing Instances (command) exists (tactic) (term) exists2 (term) existT (term) existT2 (term) export (attribute) Export (command) Expression does not evaluate to a tactic (error) Extract Constant (command) Extract Inductive (command) Extract Inlined Constant (command) Extraction (command) Extraction AutoInline (flag) Extraction Blacklist (command) Extraction Conservative Types (flag) Extraction File Comment (option) Extraction Flag (option) Extraction Implicit (command) Extraction Inline (command) Extraction KeepSingleton (flag) Extraction Language (command) Extraction Library (command) Extraction NoInline (command) Extraction Optimize (flag) Extraction Output Directory (option) Extraction SafeImplicits (flag) Extraction TestCompile (command) Extraction TypeExpand (flag)

F

f_equal (tactic) (term) f_equal2 ... f_equal5 (term) Fact (command) Fail (command) fail (tactic) Failed to progress (error) False (term) false (term) False_rec (term) False_rect (term) Fast Name Printing (flag) field (tactic) field_lookup (tactic) field_simplify (tactic) field_simplify_eq (tactic) File ... found twice in ... (warning) File not found on loadpath: ‘string’ (error) Files processed by Load cannot leave open proofs (error) Final Obligation (command) finish_timing (tactic) first (ssreflect) (tactic), [1] first (tactic) first last (tactic variant) firstorder (tactic) Firstorder Depth (option) Firstorder Solver (option) fix (tactic) Fix_eq (term)

Fix_F (term) Fix_F_eq (term) Fix_F_inv (term) Fixpoint (command) Flag 'rename' expected to rename ‘name’ into ‘name’ (error) flat_map (term) Focus (command) fold (tactic) fold_left (term) fold_right (term) forall Found a constructor of inductive type term while a constructor of term is expected (error) Found an "at" clause without "with" clause (error) Found no matching notation to enable or disable (error) Found no subterm matching ‘term’ in the current goal (error) Found no subterm matching ‘term’ in ‘ident’ (error) Found target class ‘coercion_class’ instead of ‘coercion_class’ (error) fresh (tactic) From … Dependency (command) From … Require (command) fst (term) fun (tactic) Funclass cannot be a source class (error) Function (command) function_scope Functional Case (command) functional induction (tactic) functional inversion (tactic) Functional Scheme (command)

G

ge (term) Generalizable (command) generalize (tactic) generalize dependent (tactic) generalize_eqs (tactic) generalize_eqs_vars (tactic) generally have (tactic) Generate graph for (command) gfail (tactic)

gintuition (tactic) give_up (tactic) global (attribute) Goal (command) Goal is solvable by congruence but some arguments are missing. Try congruence with ‘term’…‘term’, replacing metavariables by arbitrary terms (error) gt (term) guard (tactic) Guard Checking (flag) Guarded (command)

H

has_evar (tactic) have (tactic), [1] head (term) head_of_constr (tactic) Hint Constants (command) Hint Constructors (command) Hint Cut (command) Hint Extern (command) Hint Immediate (command) Hint Mode (command) Hint Opaque (command) Hint Resolve (command)

Hint Rewrite (command) Hint Transparent (command) Hint Unfold (command) Hint Variables (command) Hint View for (command) Hint View for apply (command), [1] Hint View for move (command) hnf (tactic) Hypotheses (command) Hypothesis (command) Hypothesis ‘ident’ must contain at least one Function (error) Hyps Limit (option)

I

I (term) I don’t know how to handle dependent equality (error) identity (term), [1] Identity Coercion (command) idtac (tactic) if-then-else (Ltac2) (tactic) IF_then_else (term) iff (term) Ignored instance declaration for “‘ident’”: “‘term’” is not a class (warning) Ignoring implicit binder declaration in unexpected position (warning) Ill-formed recursive definition (error) Ill-formed template inductive declaration: not polymorphic on any universe (error) Implicit Arguments (flag) Implicit Type (command) Implicit Types (command) Import (command) in (tactic) Include (command) Include Type (command) Incorrect number of tactics (expected N tactics, was given M) (error) induction (tactic) Inductive (command) Infix (command) Info (command) Info Auto (flag) Info Eauto (flag) Info Level (option) Info Trivial (flag) info_auto (tactic) info_eauto (tactic)

info_trivial (tactic) infoH (command) injection (tactic) inl (term) inleft (term) inr (term) inright (term) Inspect (command) Instance (command) instantiate (tactic) Instructions (command) intro (tactic) intros (tactic) intros until (tactic) intuition (tactic) Intuition Negation Unfolding (flag) Invalid backtrack (error) inversion (tactic) inversion_clear (tactic) inversion_sigma (tactic) is_cofix (tactic) is_const (tactic) is_constructor (tactic) is_evar (tactic) is_fix (tactic) is_ground (tactic) is_ind (tactic) is_proj (tactic) is_var (tactic) IsSucc (term)

K

Keep Equalities (table) Keep Proof Equalities (flag)

Kernel Term Sharing (flag) Keyed Unification (flag)

L

lapply (tactic) lapply needs a non-dependent product (error) last (tactic) Last block to end has name ‘ident’ (error) last first (tactic variant) lazy (tactic) lazy_match! (tactic) lazy_match! goal (tactic) lazymatch (tactic) lazymatch goal (tactic) le (term) le_n (term) le_S (term) left (tactic) (term) Lemma (command) length (term) Let (command) let (tactic) let ... := ... (term) Let CoFixpoint (command) Let Fixpoint (command) lia (tactic) Lia Cache (flag) Library File (transitively required) ‘qualid’ is deprecated since ‘string’. ‘string’ (warning) Library File ‘qualid’ is deprecated since ‘string’. ‘string’ (warning) Load (command) Load is not supported inside proofs (error) local (attribute) Locate (command)

Locate File (command) Locate Library (command) Locate Ltac (command) Locate Ltac2 (command) Locate Module (command) Locate Term (command) Loose Hint Behavior (option) lra (tactic) lt (term) Ltac (command) Ltac Backtrace (flag) Ltac Batch Debug (flag) Ltac Debug (flag) Ltac Profiler encountered an invalid stack (no self node). This can happen if you reset the profile during tactic execution (warning) Ltac Profiling (flag) ltac-seq (tactic) Ltac2 (command) Ltac2 alias ‘qualid’ is deprecated since ‘string’. ‘string’ (warning) Ltac2 Backtrace (flag) Ltac2 Check (command) Ltac2 definition ‘qualid’ is deprecated since ‘string’. ‘string’ (warning) Ltac2 Eval (command) Ltac2 external (command) Ltac2 Globalize (command) Ltac2 In Ltac1 Profiling (flag) Ltac2 Notation (abbreviation) (command) Ltac2 Notation (command) Ltac2 notation ‘ltac2_scope’…‘ltac2_scope’ is deprecated since ‘string’. ‘string’ (warning) Ltac2 Set (command) Ltac2 Type (command)

M

Making shadowed name of implicit argument accessible by position (warning) Mangle Names (flag) Mangle Names Light (flag) Mangle Names Prefix (option) map (term) match (Ltac2) (tactic) match (tactic) match ... with ... match goal (tactic) match! (tactic) match! goal (tactic) Maximal Implicit Insertion (flag) Missing mapping for constructor ‘qualid’ (error) mod (term) Module (command)

Module Type (command) Module/section ‘qualid’ not found (error) Monomorphic (attribute) More than one interpretation bound to this notation, confirm with the "all" modifier (error) move (ssreflect) (tactic), [1] move (tactic) mult (term) mult_n_O (term) mult_n_Sm (term) multi_match! (tactic) multi_match! goal (tactic) multimatch (tactic) multimatch goal (tactic) Multiple 'via' options (error) Multiple 'warning after' or 'abstract after' options (error)

N

n_Sn (term) nat (term) nat_case (term) nat_double_ind (term) nat_scope native_cast_no_check (tactic) native_compute (tactic) NativeCompute Profile Filename (option) NativeCompute Profiling (flag) NativeCompute Timing (flag) Nested Proofs Allowed (flag) Nested proofs are discouraged and not allowed by default. This error probably means that you forgot to close the last "Proof." with "Qed." or "Defined.". If you really intended to use nested proofs, you can do so by turning the "Nested Proofs Allowed" flag on (error) New coercion path ... is ambiguous with existing ... (warning) New Collection definition of ‘ident’ shadows the previous one (warning) Next Obligation (command) nia (tactic) Nia Cache (flag) No applicable tactic (error) No argument name ‘ident’ (error) No evars (error) No field named ‘ident’ in ‘qualid’ (error) No focused proof (error) No focused proof (No proof-editing in progress) (error) No focused proof to restart (error) No head constant to reduce (error) No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop. You can try to use option Set Keep Proof Equalities (error) No matching clauses for match (error) No matching clauses for match goal (error) No notation provided (error) No primitive equality found (error) No product even after head-reduction (error) No progress made (error) No quantified hypothesis named ‘ident’ in current goal even after head-reduction (error) No such assumption (error) No such binder (error) No such bound variable ‘ident’ (no bound variables at all in the expression) (error) No such bound variable ‘ident’ (possible names are: ‘ident’ ...) (error) No such goal (error) No such goal (‘ident’) (error) No such goal (‘natural’) (error) No such goal. (fail) (error) No such goal. (Goal selector) (error) No such goal. Focus next goal with bullet ‘bullet’ (error) No such goal. Try unfocusing with } (error) No such hypothesis: ‘ident’ (error) No ‘natural’-th non dependent hypothesis in current goal even after head-reduction (error) Non exhaustive pattern matching (error) Non extensible universe declaration not supported with monomorphic Program Definition (error) Non strictly positive occurrence of ‘ident’ in ‘type’ (error)

NonCumulative (attribute) None (term) Nonrecursive Elimination Schemes (flag) nonuniform (attribute) not (term) not a cofix definition (error) not a constant (error) not a constructor (error) Not a context variable (error) Not a discriminable equality (error) not a fix definition (error) Not a negated primitive equality (error) not a primitive projection (error) Not a valid ring equation (error) Not a variable or hypothesis (error) not an (co)inductive datatype (error) Not an evar (error) Not an exact proof (error) Not an inductive goal with 1 constructor (error) Not an inductive goal with 2 constructors (error) Not an inductive product (error) Not convertible (error) Not enough constructors (error) Not enough non implicit arguments to accept the argument bound to ‘ident’ (error) Not enough non implicit arguments to accept the argument bound to ‘natural’ (error) Not equal (due to universes) (error) Not equal (error) Not ground (error) Not the right number of induction arguments (error) Not the right number of missing arguments (expected ‘natural’) (error) not_eq_S (term) not_evar (tactic) Notation (abbreviation) (command) Notation (command) Notation levels must range between 0 and 6 (error) Notation ‘string’ is deprecated since ‘string’. ‘string’ (warning) Notations for lists Nothing to inject (error) Nothing to rewrite (error) notT (term) now (tactic) now_show (tactic) nra (tactic) Nra Cache (flag) nsatz (tactic) nsatz_compute (tactic) nth (term) Number Notation (command) numgoals (tactic)

O

O (term) O_S (term) Obligation (command) Obligation Tactic (command) Obligations (command) once (tactic) only (tactic) Opaque (command) Open Scope (command)

Optimize Heap (command) Optimize Proof (command) optimize_heap (tactic) option (term) or (term) or_introl (term) or_intror (term) over (tactic), [1] overflow in int63 literal ‘bigint’ (error)

P

package-name.foo and not foo_plugin (error) pair (term) Parameter (command) Parameters (command) Parsing Explicit (flag) pattern (tactic) Peano's arithmetic plugin name anymore. Plugins should be loaded using their (error) plus (term) plus_n_O (term) plus_n_Sm (term) Polymorphic (attribute) Polymorphic Inductive Cumulativity (flag) Polymorphic universe constraints can only be declared inside sections, use Monomorphic Constraint instead (error) Polymorphic universes can only be declared inside sections, use Monomorphic Universe instead (error) pose (ssreflect) (tactic) pose (tactic) pose proof (tactic) Positivity Checking (flag) pred (term) pred_Sn (term) Prenex Implicits (command), [1] Preterm (command) Primitive (command) Primitive Projections (flag) Print (command) Print All (command) Print All Dependencies (command) Print Assumptions (command) Print Canonical Projections (command) Print Classes (command) Print Coercion Paths (command) Print Coercions (command) Print Custom Grammar (command) Print Debug GC (command) Print Equivalent Keys (command) Print Extraction Blacklist (command) Print Extraction Inline (command) Print Fields (command) Print Firstorder Solver (command) Print Grammar (command) Print Graph (command) Print Hint (command) Print HintDb (command) Print Implicit (command) Print Instances (command) Print Keywords (command) Print Libraries (command) Print LoadPath (command) Print Ltac (command) Print Ltac Signatures (command) Print Ltac2 (command) Print Ltac2 Signatures (command) Print Ltac2 Type (command) Print ML Modules (command) Print ML Path (command) Print Module (command) Print Module Type (command) Print Namespace (command) Print Notation (command) Print Opaque Dependencies (command) Print Options (command) Print Registered (command) Print Rewrite HintDb (command) Print Rings (command) Print Scope (command) Print Scopes (command) Print Section (command) Print Strategies (command) Print Strategy (command)

Print Table (command) Print Tables (command) Print Transparent Dependencies (command) Print Typeclasses (command) Print Typing Flags (command) Print Universes (command) Print Visibility (command) Printing All (flag) Printing Allow Match Default Clause (flag) Printing Coercion (table) Printing Coercions (flag) Printing Compact Contexts (flag) Printing Constructor (table) Printing Dependent Evars Line (flag) Printing Depth (option) Printing Existential Instances (flag) Printing Factorizable Match Patterns (flag) Printing Float (flag) Printing Goal Names (flag) Printing Goal Tags (flag) Printing If (table) Printing Implicit (flag) Printing Implicit Defensive (flag) Printing Let (table) Printing Match All Subterms (flag) Printing Matching (flag) Printing Notations (flag) Printing Parentheses (flag) Printing Primitive Projection Parameters (flag) Printing Projections (flag) Printing Raw Literals (flag) Printing Record (table) Printing Records (flag) Printing Synth (flag) Printing Unfocused (flag) Printing Unfolded Projection As Match (flag) Printing Universes (flag) Printing Use Implicit Types (flag) Printing Width (option) Printing Wildcard (flag) Private (attribute) Private Polymorphic Universes (flag) private(matching) (attribute) prod (term) Program (attribute) program (attribute) Program Cases (flag) Program Generalized Coercion (flag) Program Mode (flag) Programming progress (tactic) proj1 (term) proj2 (term) projections(primitive) (attribute) projT1 (term) projT2 (term) Proof (command) Proof `term` (command) Proof is not complete. (abstract) (error) Proof is not complete. (assert) (error) Proof Mode (command) Proof using (command) Proof with (command) Prop Property (command) Proposition (command) protect_fv (tactic) psatz (tactic) Psatz (theorem) public name according to findlib, for example (error) Pwd (command)

Q

Qed (command)

Quantifiers Quit (command)

R

rapply (tactic) Record (command) Records declared with the keyword Record or Structure cannot be recursive (error) Recursion Recursive Extraction (command) Recursive Extraction Library (command) red (tactic) Redirect (command) refine (attribute) (tactic) refl_identity (term) reflexivity (tactic) Register (command) Register Inline (command) Regular Subst Tactic (flag) Remark (command) remember (tactic) Remove (command) Remove Hints (command) rename (tactic) repeat (tactic) replace (tactic) Require (command) Require Export (command) Require Import (command) Require inside a module is deprecated and strongly discouraged. You can Require a module at toplevel and optionally Import it inside another one (warning) Required library ‘qualid’ matches several files in path (found file.vo, file.vo, ...) (error) Reserved Infix (command)

Reserved Notation (command) Reset (command) Reset Extraction Blacklist (command) Reset Extraction Inline (command) Reset Initial (command) Reset Ltac Profile (command) reset ltac profile (tactic) Restart (command) restart_timer (tactic) rev (term) reversible (attribute) Reversible Pattern Implicit (flag) revert (tactic) revert dependent (tactic) revgoals (tactic) rewrite (ssreflect) (tactic) rewrite (tactic) rewrite * (tactic) rewrite_db (tactic) rewrite_strat (tactic) Rewriting Schemes (flag) right (tactic) (term) ring (tactic) Ring operation should be declared as a morphism (error) ring_lookup (tactic) ring_simplify (tactic) rtauto (tactic)

S

S (term) Save (command) Scheme (command) Scheme Boolean Equality (command) Scheme Equality (command) Scope delimiters should not start with an underscore (error) Scope names should not start with an underscore (error) Search (command) Search Blacklist (table) Search Output Name Only (flag) SearchPattern (command) SearchRewrite (command) Section (command) Section variable ‘ident’ occurs implicitly in global declaration ‘qualid’ present in hypothesis ‘ident’ (error) Section variable ‘ident’ occurs implicitly in global declaration ‘qualid’ present in the conclusion (error) sentence Separate Extraction (command) Set (command) (sort) set (ssreflect) (tactic), [1] set (tactic) setoid_etransitivity (tactic) setoid_reflexivity (tactic) setoid_replace (tactic) setoid_rewrite (tactic) setoid_symmetry (tactic) setoid_transitivity (tactic) shared library failed: Coq Error: ‘string’ is not a valid (error) shelve (tactic) shelve_unifiable (tactic) Short Module Printing (flag) Show (command) Show Conjectures (command) Show Existentials (command) Show Extraction (command) Show Goal (command) Show Intro (command) Show Intros (command) Show Lia Profile (command) Show Ltac Profile (command) show ltac profile (tactic) Show Match (command) Show Obligation Tactic (command) Show Proof (command) Show Universes (command) Show Zify (command) sig (term) sig2 (term) Signature components for field ‘ident’ do not match (error) sigT (term) sigT2 (term) Silent (flag) simpl (tactic) simple apply (tactic) simple congruence (tactic)

simple destruct (tactic) simple eapply (tactic) simple induction (tactic) simple injection (tactic) simple inversion (tactic) simple subst (tactic) simplify_eq (tactic) singel: / (term) snd (term) soft functional induction (tactic) solve (tactic) Solve All Obligations (command) Solve Obligations (command) Solve Unification Constraints (flag) solve_constraints (tactic) Some (term) specialize (tactic) specialize_eqs (tactic) split (tactic) split_Rabs (tactic) split_Rmult (tactic) SProp SProp is disallowed because the "Allow StrictProp" flag is off (error) SSReflect: cannot obtain new equations out of ... (warning) SsrHave NoTCResolution (flag) SsrIdents (flag) SsrOldRewriteGoalsOrder (flag) SsrRewrite (flag) Stack overflow or segmentation fault happens when working with large numbers in ‘type’ (threshold may vary depending on your system limits and on the command executed) (warning) start ltac profiling (tactic) stepl (tactic) stepr (tactic) stop ltac profiling (tactic) Strategy (command) Strict Implicit (flag) Strict Universe Declaration (flag) String Notation (command) Strongly Strict Implicit (flag) Structural Injection (flag) Structure (command) SubClass (command) subst (tactic) substitute (tactic) Succeed (command) suff (tactic) suffices (tactic) Suggest Proof Using (flag) sum (term) sumbool (term) sumor (term) swap (tactic) sym_not_eq (term) symmetry (tactic) Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]) (error) Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]) (error)

T

tactic Tactic failure (error) Tactic failure (level ‘natural’) (error) Tactic failure: <tactic closure> succeeds (error) Tactic failure: Setoid library not loaded (error) Tactic generated a subgoal identical to the original goal (error) Tactic Notation (command) Tactic Notation ‘qualid’ is deprecated since ‘string’. ‘string’ (warning) Tactic ‘qualid’ is deprecated since ‘string’. ‘string’ (warning) tail (term) tauto (tactic) template and polymorphism not compatible (error) term Terms do not have convertible types (error) Test (command) The "at" syntax isn't available yet for the autorewrite tactic (error) The & modifier may only occur once (error) The 'abstract after' directive has no effect when the parsing function (‘qualid’) targets an option type (warning) The 'clear implicits' flag must be omitted if implicit annotations are given (error) The 'default implicits' flag is incompatible with implicit annotations (error) The / modifier may only occur once (error) The command has not failed! (error) The conclusion of ‘type’ is not valid it must be built from ‘ident’ (error) The constant ‘number’ is not a binary64 floating-point value. A closest value ‘number’ will be used and unambiguously printed ‘number’. [inexact-float,parsing] (warning) The constructor ‘ident’ expects ‘natural’ arguments (error) The cumulative attribute can only be used in a polymorphic context (error) The elimination predicate term should be of arity ‘natural’ (for non dependent case) or ‘natural’ (for dependent case) (error) The field ‘ident’ is missing in ‘qualid’ (error) The file ‘ident’.vo contains library ‘qualid’ and not library ‘qualid’ (error) The recursive argument must be specified (error) The reference is not unfoldable (error) The reference X was not found in the current environment (error) The reference ‘qualid’ was not found in the current environment (error) The relation ‘ident’ is not a declared reflexive relation. Maybe you need to require the Coq.Classes.RelationClasses library (error) The relation ‘ident’ is not a declared symmetric relation. Maybe you need to require the Coq.Classes.RelationClasses library (error) The relation ‘ident’ is not a declared transitive relation. Maybe you need to require the Coq.Classes.RelationClasses library (error) The term "‘type’" has type "‘type’" which should be Set, Prop or Type (error) The term ‘term’ has type ‘type’ which should be Set, Prop or Type (error) The term ‘term’ has type ‘type’ while it is expected to have type ‘type’' (error) The type has no constructors (error) The type ‘ident’ must be registered before this construction can be typechecked (error) The variable ident is bound several times in pattern term (error) The variable ‘ident’ is already declared (error) The ‘natural’ th argument of ‘ident’ must be ‘ident’ in ‘type’ (error) Theorem (command) Theories There is already an Ltac named ‘qualid’ (error) There is no flag or option with this name: "‘setting_name’" (warning) There is no flag, option or table with this name: "‘setting_name’" (error)

There is no Ltac named ‘qualid’ (error) There is no qualid-valued table with this name: "‘setting_name’" (error) There is no string-valued table with this name: "‘setting_name’" (error) There is nothing to end (error) This command does not support this attribute (warning) This command is just asserting the names of arguments of ‘qualid’. If this is what you want, add ': assert' to silence the warning. If you want to clear implicit arguments, add ': clear implicits'. If you want to clear notation scopes, add ': clear scopes' (warning) This hint is not local but depends on a section variable. It will disappear when the section is closed (warning) This object does not support universe names (error) This proof is focused, but cannot be unfocused this way (error) This tactic has more than one success (error) Time (command) time (tactic) time_constr (tactic) Timeout (command) timeout (tactic) To avoid stack overflow, large numbers in ‘type’ are interpreted as applications of ‘qualid’ (warning) To rename arguments the 'rename' flag must be specified (error) transitivity (tactic) Transparent (command) Transparent Obligations (flag) transparent_abstract (tactic) trivial (tactic) True (term) true (term) try (tactic) tryif (tactic) Trying to mask the absolute name ‘qualid’! (warning) tt (term) Type type Type (command) type of (tactic) Type of ‘ident’ is not an equality of recognized Σ types: expected one of sig sig2 sigT sigT2 sigT2 ex or ex2 but got ‘term’ (error) Type of ‘qualid’ seems incompatible with the type of ‘qualid’. Expected type is: ‘type’ instead of ‘type’. This might yield ill typed terms when using the notation (warning) type_scope type_term (tactic) Typeclass Resolution For Conversion (flag) Typeclasses Debug (flag) Typeclasses Debug Verbosity (option) Typeclasses Dependency Order (flag) Typeclasses Depth (option) Typeclasses eauto (command) typeclasses eauto (tactic) Typeclasses Iterative Deepening (flag) Typeclasses Limit Intros (flag) Typeclasses Opaque (command) Typeclasses Strict Resolution (flag) Typeclasses Transparent (command) Typeclasses Unique Instances (flag) Typeclasses Unique Solutions (flag)

U

Unable to apply lemma of type "..." on hypothesis of type "..." (error) Unable to find an instance for the variables ‘ident’ … ‘ident’ (error) Unable to find an instance for the variables ‘ident’…‘ident’ (error) Unable to infer a match predicate (error) Unable to satisfy the rewriting constraints (error) Unable to unify ‘one_term’ with ‘one_term’ (error) Unbound [value|constructor] X (error) Unbound context identifier ‘ident’ (error) Undeclared universe ‘ident’ (error) Undelimit Scope (command) under (tactic), [1] Undo (command) Unexpected non-option term ‘term’ while parsing a number notation (error) Unexpected non-option term ‘term’ while parsing a string notation (error) Unexpected only parsing for an only printing notation (error) Unexpected only printing for an only parsing notation (error) Unexpected term ‘term’ while parsing a number notation (error) Unexpected term ‘term’ while parsing a string notation (error) Unfocus (command) Unfocused (command) unfold (tactic) Uniform Inductive Parameters (flag)

unify (tactic) unit (term) Universe (command) Universe Checking (flag) Universe inconsistency (error) Universe instance length is ‘natural’ but should be ‘natural’ (error) Universe Minimization ToSet (flag) Universe Polymorphism (flag) Universes (command) universes(cumulative) (attribute) universes(polymorphic) (attribute) universes(template) (attribute) Unknown custom entry (error) Unknown custom entry: ‘ident’ (error) Unknown inductive type (error) unlock (tactic), [1] Unset (command) Unshelve (command) unshelve (tactic) Unterminated string in notation (error) Unused variable ‘ident’ might be a misspelled constructor. Use _ or _‘ident’ to silence this warning (warning) Use of ‘string’ Notation is deprecated as it is inconsistent with pattern syntax (warning) using (attribute)

V

Validate Proof (command) value (term) Variable (command) Variable All is shadowed by Collection named All containing all variables (warning)

Variables (command) Variant (command) vm_cast_no_check (tactic) vm_compute (tactic)

W

warning (attribute) warnings (attribute) Warnings (option) Well founded induction Well foundedness well_founded (term) with_strategy (tactic) without loss (tactic) wlia (tactic) wlog (tactic), [1]

wlra_Q (tactic) wnia (tactic) wnra_Q (tactic) wpsatz_Q (tactic) wpsatz_Z (tactic) Wrong argument name (error) Wrong argument position (error) Wrong bullet ‘bullet’: Bullet ‘bullet’ is mandatory here (error) Wrong bullet ‘bullet’: Current bullet ‘bullet’ is not finished (error) wsos_Q (tactic) wsos_Z (tactic)

X

xlia (tactic) xlra_Q (tactic) xlra_R (tactic) xnia (tactic) xnra_Q (tactic) xnra_R (tactic)

xpsatz_Q (tactic) xpsatz_R (tactic) xpsatz_Z (tactic) xsos_Q (tactic) xsos_R (tactic) xsos_Z (tactic)

Z

zify (tactic) zify_elim_let (tactic) zify_iter_let (tactic)

zify_iter_specs (tactic) zify_op (tactic) zify_saturate (tactic)