Index

Symbols

* (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) @ident already exists. (Axiom) (error)

@ident already exists. (Definition) (error) @ident already exists. (Program Definition) (error) @ident already exists. (Theorem) (error) [ … | … | … ] (dispatch) (tactic) [> … | … | … ] (dispatch) (tactic) `( ) `(! ) `[ ] `[! ] `{ } `{! } { {A}+{B} (term) {x:A & P x} (term) {x:A | P x} (term) || (first tactic making progress) (tactic) }

_

_

A

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) Add (command) Add Field (command) Add LoadPath (command) Add ML Path (command) Add Morphism (command) Add Parametric Morphism (command) Add Parametric Relation (command) Add Rec LoadPath (command) Add Relation (command) Add Ring (command) Add Setoid (command) 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) apply … in (tactic) apply … in … as (tactic variant) 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 of ring_simplify do not have all the same type (error) Arithmetical notations assert (tactic) assert_fails (tactic) assert_succeeds (tactic) assumption (tactic) Asymmetric Patterns (flag) Attempt to save an incomplete proof (error) auto (tactic) Auto Template Polymorphism (flag) autoapply (tactic) Automatically declaring ‘ident’ as template polymorphic (warning) autorewrite (tactic) autounfold (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) Bracketing Last Introduction Pattern (flag) Brackets do not support multi-goal selectors (error) btauto (tactic) Bullet Behavior (option) by (tactic)

C

Cannot build functional inversion principle (warning) 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 any non-recursive equality over :n:`‘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 handle mutually (co)inductive records (error) 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 ‘class’ as a source class of ‘qualid’ (error) Cannot use mutual definition with well-founded recursion or measure (error) canonical (attribute) Canonical Structure (command) canonical(false) (attribute) Can’t find file ‘ident’ on loadpath (error) case (ssreflect) (tactic) case (tactic) Case Analysis Schemes (flag) 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)

clearbody (tactic variant) 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 variant) Condition not satisfied (error) congr (tactic), [1] congruence (tactic) Congruence Verbose (flag) congruence with (tactic variant) conj (term) Conjecture (command) Conjectures (command) Connectives constr_eq (tactic) constr_eq_strict (tactic) Constraint (command) constructor (tactic) Context (command) context (tactic) Contextual Implicit (flag) contradict (tactic) contradiction (tactic) convert_concl_no_check (tactic variant) Coqtop Exit On Error (flag) Corollary (command) Create HintDb (command) Cumulative StrictProp (flag) Cumulativity Weak Constraints (flag) cut (tactic variant) cutrewrite (tactic variant) cycle (tactic)

D

Datatypes Debug Auto (flag) debug auto (tactic variant) Debug Cbv (flag) Debug Eauto (flag) Debug mode not available in the IDE (error) Debug RAKAM (flag) Debug Ssreflect (flag) Debug SsrMatching (flag) Debug Tactic Unification (flag) Debug Trivial (flag) debug trivial (tactic variant) Debug Unification (flag) Decidable Equality Schemes (flag) decide equality (tactic) Declare Custom Entry (command) Declare Instance (command variant) Declare Left Step (command) Declare ML Module (command) Declare Module (command) Declare Morphism (command) Declare Reduction (command) Declare Right Step (command) Declare Scope (command) decompose (tactic) Default Goal Selector (option) Default Proof Mode (option)

Default Proof Using (option) Default Timeout (option) Defined (command) Definition (command) Delimit Scope (command) dependent destruction (tactic variant) dependent induction (tactic) dependent inversion (tactic variant) dependent inversion … with … (tactic variant) dependent rewrite -> (tactic) dependent rewrite <- (tactic variant) deprecated (attribute) Derive (command) Derive Inversion (command) destruct (tactic) destruct … eqn: (tactic variant) Diffs (option) dintuition (tactic variant) discriminate (tactic) discrR (tactic) do (ssreflect) (tactic) do (tactic) done (tactic) double induction (tactic) Drop (command) dtauto (tactic variant) Dump Arith (option)

E

eapply (tactic variant) eassert (tactic variant) eassumption (tactic variant) easy (tactic) eauto (tactic) ecase (tactic variant) econstructor (tactic variant) edestruct (tactic variant) ediscriminate (tactic variant) eelim (tactic variant) eenough (tactic variant) eexact (tactic variant) eexists (tactic variant) einduction (tactic variant) einjection (tactic variant) eintros (tactic) Either there is a type incompatibility or the problem involves dependencies (error) Elaboration StrictProp Cumulativity (flag) eleft (tactic variant) elim (ssreflect) (tactic) elim (tactic variant) elim … with (tactic variant) Elimination Schemes (flag) elimtype (tactic variant) End (command) enough (tactic variant) epose (tactic variant) epose proof (tactic variant) 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 variant) erewrite (tactic variant) eright (tactic variant) error (term) eset (tactic variant) esimplify_eq (tactic variant)

esplit (tactic variant) 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) Existential (command) Existing Instance (command) exists (tactic variant) (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), [1] 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 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_simplify (tactic) field_simplify_eq (tactic) File not found on loadpath: ‘string’ (error) Files processed by Load cannot leave open proofs (error) 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) flat_map (term) Focus (command) fold (tactic) fold_left (term) fold_right (term) forall Found target class ... instead of ... (error) fresh (tactic) From … Require (command) fst (term) fun (tactic) Funclass cannot be a source class (error) Function (command) function_scope functional induction (tactic) functional inversion (tactic) Functional Scheme (command)

G

ge (term) Generalizable (command) generalize (tactic) generally have (tactic) gfail (tactic) give_up (tactic) global (attribute)

Goal (command) goal does not satisfy the expected preconditions (error) Goal is solvable by congruence but some arguments are missing. Try congruence with ‘term’…‘term’, replacing metavariables by arbitrary terms (error) Grab Existential Variables (command) gt (term) guard (tactic) Guard Checking (flag) Guarded (command)

H

has_evar (tactic) have (tactic), [1] head (term) Hide Obligations (flag) Hint (command) Hint Constants (command variant) Hint Constructors (command variant) Hint Cut (command variant) Hint Extern (command variant) Hint Immediate (command variant) Hint Mode (command variant) Hint Opaque (command variant)

Hint Resolve (command variant) Hint Rewrite (command), [1], [2], [3] Hint Transparent (command variant) Hint Unfold (command variant) Hint Variables (command variant) 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 (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) In environment … the term: ‘term’ does not have type ‘type’. Actually, it has type ... (error) Include (command) Include Type (command) Incorrect number of tactics (expected N tactics, was given M) (error) induction (tactic) induction … using … (tactic variant) Inductive (command) Infix (command) Info (command) Info Auto (flag)

Info Eauto (flag) Info Level (option) Info Trivial (flag) info_trivial (tactic variant) infoH (tactic) injection (tactic) inl (term) inleft (term) inr (term) inright (term) Inspect (command) Instance (command) instantiate (tactic) intro (tactic) intros (tactic variant) intros … (tactic) intuition (tactic) Intuition Negation Unfolding (flag) Invalid argument (error) Invalid backtrack (error) inversion (tactic) inversion ... using ... (tactic) inversion_clear (tactic variant) inversion_sigma (tactic variant) is_evar (tactic) is_var (tactic) IsSucc (term)

K

Keep Proof Equalities (flag)

Keyed Unification (flag)

L

lapply (tactic variant) last (tactic) Last block to end has name ‘ident’ (error) last first (tactic variant) lazy (tactic) lazymatch (tactic) lazymatch goal (tactic) le (term) le_n (term) le_S (term) left (tactic variant) (term) Lemma (command) length (term) Let (command) let (tactic) let ... := ... (term) Let CoFixpoint (command) Let Fixpoint (command) lia (tactic) Lia Cache (flag) Load (command) Load is not supported inside proofs (error)

local (attribute) Locate (command) Locate File (command) Locate Library (command) Locate Ltac (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 Backtrace (flag) Ltac2 Eval (command) Ltac2 Notation (command) Ltac2 Set (command) Ltac2 Type (command)

M

Making shadowed name of implicit argument accessible by position (warning) Mangle Names (flag) Mangle Names Prefix (option) map (term) match (tactic) match ... with ... match goal (tactic) Maximal Implicit Insertion (flag) mod (term) Module (command) Module Type (command)

Module/section ‘qualid’ not found (error) move (tactic), [1] move … after … (tactic) move … at bottom (tactic variant) move … at top (tactic variant) move … before … (tactic variant) mult (term) mult_n_O (term) mult_n_Sm (term) multimatch (tactic) multimatch goal (tactic)

N

n_Sn (term) nat (term) nat_case (term) nat_double_ind (term) nat_scope native_cast_no_check (tactic variant) native_compute (tactic variant) NativeCompute Profile Filename (option) NativeCompute Profiling (flag) NativeCompute Timing (flag) Nested Proofs Allowed (flag) Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on (error) New coercion path ... is ambiguous with existing ... (warning) Next Obligation (command) nia (tactic) Nia Cache (flag) No applicable tactic (error) No argument name ‘ident’ (error) No discriminable equalities (error) No evars (error) No focused proof (error), [1] No focused proof (No proof-editing in progress) (error) No focused proof to restart (error) No head constant to reduce (error) No matching clauses for match (error) No matching clauses for match goal (error) No primitive equality found (error) No product even after head-reduction (error) No progress made (error) No such assumption (error), [1] No such binder (error) No such goal (error) No such goal (‘ident’) (error) No such goal (‘num’) (error) No such goal. (fail) (error) No such goal. (Goal selector) (error) No such goal. Focus next goal with bullet ‘bullet’ (error) No such hypothesis (error), [1], [2], [3] No such hypothesis in current goal (error), [1] No such hypothesis: ‘ident’ (error), [1] No such label ‘ident’ (error)

Non exhaustive pattern matching (error) Non strictly positive occurrence of ‘ident’ in ‘type’ (error) None (term) Nonrecursive Elimination Schemes (flag) not (term) Not a context variable (error) Not a discriminable equality (error) Not a primitive equality (error) Not a projectable equality but a discriminable one (error) Not a proposition or a type (error) Not a valid ring equation (error) Not a variable or hypothesis (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), [1] Not convertible (error) Not enough constructors (error) Not equal (due to universes) (error), [1] Not equal (error), [1] Not reducible (error) Not the right number of induction arguments (error) Not the right number of missing arguments (error), [1] not_eq_S (term) Notation (abbreviation) (command) Notation (command) Notation ‘string’ is deprecated since ‘string’. ‘string’ (warning) Notations for lists Nothing to do, it is an equality between convertible terms (error) Nothing to inject (error) Nothing to rewrite (error) notT (term) notypeclasses refine (tactic variant) now (tactic variant) nra (tactic) Nra Cache (flag) nsatz (tactic) nth (term) Numeral Notation (command) numgoals (tactic)

O

O (term) O_S (term) Obligation (command) Obligation Tactic (command) Obligations (command) omega (tactic) Omega Action (flag) omega can't solve this system (error) Omega System (flag) Omega UseLocalDefs (flag) omega: Can't solve a goal with equality on type ... (error) omega: Can't solve a goal with non-linear products (error) omega: Can't solve a goal with proposition variables (error) omega: Not a quantifier-free goal (error)

omega: Unrecognized atomic proposition: ... (error) omega: Unrecognized predicate or connective: ‘ident’ (error) omega: Unrecognized proposition (error) 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]

P

pair (term) Parameter (command) Parameters (command) Parsing Explicit (flag) pattern (tactic) Peano's arithmetic plus (term) plus_n_O (term) plus_n_Sm (term) Polymorphic Constraint (command) Polymorphic Inductive Cumulativity (flag) Polymorphic Universe (command) 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 variant) 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 Extraction Blacklist (command) Print Extraction Inline (command) Print Firstorder Solver (command) Print Grammar (command) Print Graph (command) Print Hint (command), [1], [2], [3] Print HintDb (command) Print Implicit (command) Print Instances (command) Print Libraries (command) Print LoadPath (command) Print Ltac (command) Print Ltac Signatures (command) Print ML Modules (command) Print ML Path (command) Print Module (command) Print Module Type (command) Print Opaque Dependencies (command) Print Options (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 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 If (table) Printing Implicit (flag) Printing Implicit Defensive (flag) Printing Let (table) Printing Matching (flag) Printing Notations (flag) Printing Parentheses (flag) Printing Primitive Projection Parameters (flag) Printing Projections (flag) Printing Record (table) Printing Records (flag) Printing Synth (flag) Printing Unfocused (flag) Printing Universes (flag) Printing Use Implicit Types (flag) Printing Width (option) Printing Wildcard (flag) Private Polymorphic Universes (flag) private(matching) (attribute) prod (term) program (attribute) Program Cases (flag) Program Definition (command) Program Fixpoint (command) Program Generalized Coercion (flag) Program Lemma (command) Program Mode (flag) Programming progress (tactic) proj1 (term) proj2 (term) projT1 (term) projT2 (term) Proof (command) Proof `term` (command) Proof is not complete. (abstract) (error) Proof is not complete. (assert) (error) Proof using (command) Proof with (command) Prop Property (command) Proposition (command) psatz (tactic) Pwd (command)

Q

Qed (command)

Quantifiers Quit (command)

R

rapply (tactic variant) 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) Refine passed ill-formed term (error) refl_identity (term) reflexivity (tactic) Register (command) Register Inline (command) Regular Subst Tactic (flag) Remark (command) remember (tactic) Remove (command) Remove Hints (command) Remove LoadPath (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) 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 variant) restart_timer (tactic) rev (term) Reversible Pattern Implicit (flag) revert (tactic) revert dependent (tactic variant) revgoals (tactic) rewrite (ssreflect) (tactic) rewrite (tactic) rewrite_strat (tactic) Rewriting Schemes (flag) right (tactic variant) (term) ring (tactic) Ring operation should be declared as a morphism (error) ring_simplify (tactic) rtauto (tactic)

S

S (term) Save (command) Scheme (command) Scheme Equality (command variant) Search (command) Search (ssreflect) (command) Search Blacklist (table) Search Output Name Only (flag) SearchHead (command) SearchPattern (command) SearchRewrite (command) Section (command) Section variable :n:`‘ident’` occurs implicitly in global declaration :n:`‘qualid’` present in hypothesis :n:`‘ident’` (error) Section variable :n:`‘ident’` occurs implicitly in global declaration :n:`‘qualid’` present in the conclusion (error) sentence Separate Extraction (command) Set (command) (sort) set (ssreflect) (tactic), [1] set (tactic) setoid_reflexivity (tactic variant) setoid_replace (tactic variant) setoid_rewrite (tactic variant) setoid_symmetry (tactic variant) setoid_transitivity (tactic variant) shelve (tactic) shelve_unifiable (tactic variant) Short Module Printing (flag) Show (command) Show Conjectures (command variant) Show Existentials (command variant) Show Goal (command variant) Show Intro (command variant) Show Intros (command variant) Show Lia Profile (command) Show Ltac Profile (command) show ltac profile (tactic) Show Obligation Tactic (command) Show Proof (command variant) Show Universes (command variant) Show Zify BinOp (command) Show Zify BinRel (command) Show Zify CstOp (command) Show Zify InjTyp (command) Show Zify Spec (command) Show Zify UnOp (command) sig (term) sig2 (term) Signature components for label ‘ident’ do not match (error) sigT (term) sigT2 (term) Silent (flag) simpl (tactic)

simple apply (tactic variant) simple destruct (tactic variant) simple eapply (tactic variant) simple induction (tactic variant) simple inversion (tactic variant) simple notypeclasses refine (tactic variant) simple refine (tactic variant) Simplex (flag) simplify_eq (tactic) singel: / (term) snd (term) solve (tactic) Solve All Obligations (command) Solve Obligations (command) Solve Unification Constraints (flag) solve_constraints (tactic) Some (term) specialize (tactic variant) split (tactic variant) split_Rabs (tactic) split_Rmult (tactic) SProp SProp is disallowed because the "Allow StrictProp" flag is off (error) SsrHave NoTCResolution (flag) SsrIdents (flag) SsrOldRewriteGoalsOrder (flag) SsrRewrite (flag) Stable Omega (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) Statement without assumptions (error) stepl (tactic) stepr (tactic variant) 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) 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 ‘num’) (error) Tactic failure: <tactic closure> fails (error) Tactic failure: <tactic closure> succeeds (error) Tactic generated a subgoal identical to the original goal. This happens if ‘term’ does not occur in the 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 & modifier may only occur once (error) The 'abstract after' directive has no effect when the parsing function (‘qualid’) targets an option type (warning) The / modifier may only occur once (error) The command has not failed! (error) The conclusion is not a substitutive equation (error) The conclusion of ‘type’ is not valid it must be built from ‘ident’ (error) The constant ‘numeral’ is not a binary64 floating-point value. A closest value will be used and unambiguously printed ‘numeral’. [inexact-float,parsing] (warning) The constructor ‘ident’ expects ‘num’ arguments (error) The cumulative and noncumulative attributes can only be used in a polymorphic context (error) The elimination predicate term should be of arity ‘num’ (for non dependent case) or ‘num’ (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 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 ‘ident’ must be registered before this construction can be typechecked (error) The variable ‘ident’ is already defined (error) The ‘num’ th argument of ‘ident’ must be ‘ident’ in ‘type’ (error) The ‘term’ provided does not end with an equation (error) Theorem (command) Theories 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 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 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) Too few occurrences (error), [1] transitivity (tactic) Transparent (command) Transparent Obligations (flag) transparent_abstract (tactic) trivial (tactic variant) True (term) true (term) try (tactic) tryif (tactic) Trying to mask the absolute name ‘qualid’! (warning) tt (term) Type type type of (tactic) 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 Filtered Unification (flag) 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 (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 ... with ... (error) Unable to unify ‘term’ with ‘term’ (error), [1] 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 numeral notation (error) Unexpected non-option term ‘term’ while parsing a string notation (error) Unexpected term ‘term’ while parsing a numeral 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) Universal Lemma Under Conjunction (flag) Universe (command) Universe Checking (flag) Universe inconsistency (error) Universe instance should have length ‘num’ (error) Universe Minimization ToSet (flag) Universe Polymorphism (flag) universes(cumulative) (attribute) universes(monomorphic) (attribute) universes(noncumulative) (attribute) universes(notemplate) (attribute) universes(polymorphic) (attribute) universes(template) (attribute) Unknown inductive type (error) unlock (tactic), [1] Unset (command) Unshelve (command) unshelve (tactic) Use of ‘string’ Notation is deprecated as it is inconsistent with pattern syntax (warning)

V

value (term) Variable (command) Variable ‘ident’ is already declared (error)

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

W

Warnings (option) Well founded induction Well foundedness well_founded (term) When ‘term’ contains more than one non dependent product the tactic lapply only takes into account the first product (warning)

with_strategy (tactic) without loss (tactic) wlog (tactic), [1] Wrong bullet ‘bullet’: Bullet ‘bullet’ is mandatory here (error) Wrong bullet ‘bullet’: Current bullet ‘bullet’ is not finished (error)

Y

You should use the “Proof using [...].” syntax instead of “Proof.” to enable skipping this proof which is located inside a section. Give as argument to “Proof using” the list of section variables that are not needed to typecheck the statement but that are required by the proof (warning)

Z

zify (tactic)

Symbols

‘class’ must be a transparent constant (error) ‘ident’ cannot be defined (warning) ‘ident’ is already declared as a typeclass (warning) ‘ident’ is already used (error), [1] ‘ident’ is declared as a local axiom (warning) ‘ident’ is not a local definition (error) ‘ident’ is used in conclusion (error) ‘ident’ is used in hypothesis ‘ident’ (error) ‘ident’ is used in the conclusion (error) ‘ident’ is used in the hypothesis ‘ident’ (error), [1] ‘ident’: no such entry (error) ‘qualid’ cannot be used as a hint (error), [1] ‘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 Numeral.int to ‘type’ or (option ‘type’). Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 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 Numeral.int or (option Numeral.int). Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first) (error) ‘type’ is not an inductive type (error) … : … (goal selector) (tactic) … : … (ssreflect) (tactic)