索引

記号

* (term), [1] + (backtracking branching) (tacn) + (term), [1] - (term) ... : ... (goal selector) (tacn) ... : ... (ssreflect) (tacn) ... : ... (type cast) ... <: ... ... <<: ... < (term) <= (term) => (tacn) > (term) >= (term) ?= (term)

@ident already exists. (Axiom) (err) @ident already exists. (Definition) (err) @ident already exists. (Let) (err) @ident already exists. (Program Definition) (err) @ident already exists. (Theorem) (err) @ident already exists. (Variable) (err) [> ... | ... | ... ] (dispatch) (tacn) `( ) `{ } { {A}+{B} (term) {x:A & P x} (term) {x:A | P x} (term) || (left-biased branching) (tacn) }

_

_

A

A*B (term) A+B (term) A+{B} (term) Abort (cmd) About (cmd) abstract (ssreflect) (tacn) abstract (tacn) absurd (tacn) (term) absurd_set (term) Acc (term) Acc_inv (term) Acc_rect (term) Add @table (cmd) Add Field (cmd) Add LoadPath (cmd) Add ML Path (cmd) Add Morphism (cmd) Add Parametric Morphism (cmd) Add Parametric Relation (cmd) Add Rec LoadPath (cmd) Add Rec ML Path (cmd) Add Relation (cmd) Add Ring (cmd) Add Setoid (cmd) admit (tacn) Admit Obligations (cmd) Admitted (cmd) all (term)

all: ... (tacnv) Ambiguous path (warn) and (term) and_rect (term) app (term) apply (ssreflect) (tacn) apply (tacn) apply ... in (tacn) apply ... in ... as (tacnv) Argument of match does not evaluate to a term (err) Arguments (cmd), [1], [2] Arguments (implicits) (cmd) Arguments (scopes) (cmd) Arguments of ring_simplify do not have all the same type (err) Arithmetical notations assert (tacn) assert_fails (tacn) assert_succeeds (tacn) assumption (tacn) Asymmetric Patterns (flag) Attempt to save an incomplete proof (err) auto (tacn) autoapply (tacn) Automatic Coercions Import (flag) Automatic Introduction (flag) autorewrite (tacn) autounfold (tacn) Axiom (cmdv) Axioms (cmdv)

B

Back (cmd) BackTo (cmd) Backtrack (cmdv) Bad lemma for decidability of equality (err) Bad magic number (err) Bad occurrence number of ‘qualid’ (err) Bad ring structure (err) Bind Scope (cmd)

bool (term) bool_choice (term) Boolean Equality Schemes (flag) Bracketing Last Introduction Pattern (flag) Brackets only support the single numbered goal selector (err) btauto (tacn) Bullet Behavior (opt) by (tacn)

C

Cannot build functional inversion principle (warn) Cannot define graph for ‘ident’ (warn) Cannot define principle(s) for ‘ident’ (warn) Cannot find a declared ring structure for equality ‘term’ (err) Cannot find a declared ring structure over ‘term’ (err) Cannot find induction information on ‘qualid’ (err) Cannot find inversion information for hypothesis ‘ident’ (err) Cannot find library foo in loadpath (err) Cannot find the source class of ‘qualid’ (err) Cannot handle mutually (co)inductive records (err) Cannot infer a term for this placeholder. (Casual use of implicit arguments) (err) Cannot infer a term for this placeholder. (refine) (err) Cannot load qualid: no physical path bound to dirpath (err) Cannot move ‘ident’ after ‘ident’: it depends on ‘ident’ (err) Cannot move ‘ident’ after ‘ident’: it occurs in the type of ‘ident’ (err) Cannot recognize a boolean equality (err) Cannot recognize ‘class’ as a source class of ‘qualid’ (err) Cannot solve the goal (err) Cannot use mutual definition with well-founded recursion or measure (err) Canonical Structure (cmd) Can’t find file ‘ident’ on loadpath (err) case (ssreflect) (tacnv) case (tacn) Case Analysis Schemes (flag) cbn (tacn) cbv (tacn) Cd (cmd) change (tacn) Check (cmd) Choice (term) Choice2 (term) Class (cmd), [1] classical_left (tacn) classical_right (tacnv) clear (tacn)

clearbody (tacnv) Close Scope (cmd) Coercion (cmd) cofix (tacn) CoFixpoint (cmd) CoInductive (cmd) Collection (cmd) Combined Scheme (cmd) compare (tacn) Compiled library ‘ident’.vo makes inconsistent assumptions over library qualid (err) Compute (cmd) compute (tacn) Condition not satisfied (err) congr (tacn) congruence (tacn) Congruence Verbose (flag) congruence with (tacnv) conj (term) Conjecture (cmdv) Conjectures (cmdv) Connectives constr_eq (tacn) Constraint (cmd) constructor (tacn) Context (cmd) Contextual Implicit (flag) contradict (tacn) contradiction (tacn) Corollary (cmdv) Create HintDb (cmd) Cumulative (cmd) Cumulativity Weak Constraints (flag) cut (tacnv) cutrewrite (tacnv) cycle (tacn)

D

Datatypes Debug Auto (flag) debug auto (tacnv) Debug Cbv (flag) Debug Eauto (flag) Debug mode not available in the IDE (err) Debug RAKAM (flag) Debug Trivial (flag) debug trivial (tacnv) Decidable Equality Schemes (flag) decide equality (tacn) Declare Implicit Tactic (cmd) Declare Instance (cmdv) Declare Left Step (cmd) Declare ML Module (cmd) Declare Module (cmd) Declare Reduction (cmd) Declare Right Step (cmd) decompose (tacn) Default Goal Selector (opt) Default Proof Using (opt) Default Timeout (opt)

Defined (cmdv) Definition (cmd) Delimit Scope (cmd) dependent destruction (tacnv) dependent induction (tacn) dependent inversion (tacnv) dependent inversion ... with ... (tacnv) dependent rewrite -> (tacn) dependent rewrite <- (tacnv) Derive (cmd) Derive Inversion (cmd) destruct (tacn) destruct ... eqn: (tacnv) dintuition (tacnv) discriminate (tacn) discrR (tacn) do (ssreflect) (tacn) do (tacn) done (tacn) double induction (tacn) Drop (cmd) dtauto (tacnv)

E

eapply (tacnv) eassert (tacnv) eassumption (tacnv) easy (tacn) eauto (tacn) ecase (tacnv) econstructor (tacnv) edestruct (tacnv) ediscriminate (tacnv) eelim (tacnv) eenough (tacnv) eexact (tacnv) eexists (tacnv) einduction (tacnv) einjection (tacnv) Either there is a type incompatibility or the problem involves dependencies (err) eleft (tacnv) elim (ssreflect) (tacn) elim (tacnv) elim ... with (tacnv) Elimination Schemes (flag) elimtype (tacnv) End (cmd), [1], [2] enough (tacnv) epose (tacnv) 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 (tacnv) erewrite (tacnv) eright (tacnv) error (term) eset (tacnv)

esimplify_eq (tacnv) esplit (tacnv) Eval (cmd) evar (tacn) ex (term) ex2 (term) ex_intro (term) ex_intro2 (term) exact (tacn) exactly_once (tacn) Example (cmdv) Exc (term) exfalso (tacn) exist (term) exist2 (term) Existential (cmd) Existing Class (cmd) Existing Instance (cmd) exists (tacnv) (term) exists2 (term) existT (term) existT2 (term) Export (cmdv) Extract Constant (cmd) Extract Inductive (cmd) Extract Inlined Constant (cmd) Extraction (cmd), [1] Extraction AutoInline (flag) Extraction Blacklist (cmd) Extraction Conservative Types (flag) Extraction Implicit (cmd) Extraction Inline (cmd) Extraction KeepSingleton (flag) Extraction Language Haskell (cmd) Extraction Language OCaml (cmd) Extraction Language Scheme (cmd) Extraction Library (cmd) Extraction NoInline (cmd) Extraction Optimize (flag) Extraction SafeImplicits (flag) Extraction TestCompile (cmd)

F

f_equal (tacn) (term) f_equal2 ... f_equal5 (term) Fact (cmdv) Fail (cmd) fail (tacn) Failed to progress (err) False (term) false (term) False_rec (term) False_rect (term) field (tacn) field_simplify (tacn) field_simplify_eq (tacn) File not found on loadpath: ‘string’ (err) Files processed by Load cannot leave open proofs (err) finish_timing (tacn) first (ssreflect) (tacn) first (tacn) first last (tacn) firstorder (tacn) Firstorder Depth (opt) Firstorder Solver (opt)

fix (tacn) fix_eq (term) Fix_F (term) Fix_F_eq (term) Fix_F_inv (term) Fixpoint (cmd) flat_map (term) Focus (cmd) fold (tacn) fold_left (term) fold_right (term) forall Found target class ... instead of ... (err) fourier (tacn) fst (term) fun ... => ... Funclass cannot be a source class (err) Function (cmd) function induction (tacn) function_scope functional inversion (tacn) Functional Scheme (cmd)

G

ge (term) Generalizable (cmd) Generalizable All Variables (cmd) Generalizable No Variables (cmd) generalize (tacn) generally have (tacnv) gfail (tacnv) give_up (tacn) Global (cmd) Global Close Scope (cmd)

Global Generalizable (cmd) Global Opaque (cmdv) Global Open Scope (cmd) Global Transparent (cmdv) Goal (cmd) goal does not satisfy the expected preconditions (err) Goal is solvable by congruence but some arguments are missing. Try congruence with ‘term’…‘term’, replacing metavariables by arbitrary terms (err) Grab Existential Variables (cmd) gt (term) guard (tacn) Guarded (cmd)

H

has_evar (tacn) have (tacn) head (term) Hide Obligations (flag) Hint ( Transparent | Opaque ) (cmdv) Hint (cmd) Hint Constructors (cmdv) Hint Extern (cmdv) Hint Immediate (cmdv) Hint Resolve (cmdv)

Hint Rewrite (cmd), [1], [2], [3] Hint Unfold (cmdv) Hint View for (cmd) Hint View for apply (cmd), [1], [2] Hint View for move (cmd) hnf (tacn) Hypotheses (cmdv) Hypothesis (cmdv) Hypothesis ‘ident’ must contain at least one Function (err) Hyps Limit (opt)

I

I (term) I don’t know how to handle dependent equality (err) identity (term), [1] Identity Coercion (cmd) idtac (tacn) IF_then_else (term) iff (term) Ill-formed recursive definition (err) Implicit Arguments (flag) Implicit Types (cmd) Import (cmd) in (tacn) In environment … the term: ‘term’ does not have type ‘type’. Actually, it has type ... (err) Include (cmd), [1], [2], [3] induction (tacn) induction ... using ... (tacnv) Inductive (cmd) Infix (cmd) Info (cmd) Info Auto (flag) Info Eauto (flag) Info Level (opt)

Info Trivial (flag) info_trivial (tacnv) injection (tacn) inl (term) inleft (term) Inline (cmd) inr (term) inright (term) Inspect (cmdv) Instance (cmd) instantiate (tacn) intro (tacn) intros (tacnv) intros ... (tacn) intuition (tacn) Intuition Negation Unfolding (flag) Invalid argument (err) Invalid backtrack (err), [1] inversion (tacn) is_evar (tacn) is_var (tacn) IsSucc (term)

K

Keep Proof Equalities (flag)

L

lapply (tacnv) last (tacn) last first (tacn) lazy (tacn) le (term) le_n (term) le_S (term) left (tacnv) (term) Lemma (cmdv) length (term) Let (cmd) let ... := ... (tacn) (term) Let CoFixpoint (cmdv) Let Fixpoint (cmdv) lia (tacn) Load (cmd)

Load is not supported inside proofs (err) Loading of ML object file forbidden in a native Coq (err) Local (cmd) Local Close Scope (cmd) Local Definition (cmdv) Local Notation (cmd) Local Open Scope (cmd) Local Parameter (cmdv) Locate (cmd) Locate File (cmd) Locate Library (cmd) Loose Hint Behavior (opt) lra (tacn) lt (term) Ltac (cmd) Ltac Batch Debug (flag) Ltac Debug (flag) Ltac Profiling (flag) ltac-seq (tacn)

M

map (term) match ... with ... match goal (tacn) Maximal Implicit Insertion (flag) mod (term) Module (cmd), [1] Module Type (cmd), [1] Module/section ‘qualid’ not found (err)

Monomorphic (cmd) move (tacn) move ... after ... (tacn) move ... at bottom (tacnv) move ... at top (tacnv) move ... before ... (tacnv) mult (term) mult_n_O (term) mult_n_Sm (term)

N

n_Sn (term) nat (term) nat_case (term) nat_double_ind (term) nat_scope native_compute (tacnv) NativeCompute Profile Filename (opt) NativeCompute Profiling (flag) Next Obligation (cmd) nia (tacn) No applicable tactic (err) No argument name ‘ident’ (err) No discriminable equalities (err) No evars (err) No focused proof (err), [1] No focused proof (No proof-editing in progress) (err) No focused proof to restart (err) No head constant to reduce (err) No matching clauses for match (err) No matching clauses for match goal (err) No primitive equality found (err) No product even after head-reduction (err) No progress made (err) No such assumption (err), [1] No such binder (err) No such goal (err) No such goal. (fail) (err) No such goal. (Focusing) (err) No such goal. (Goal selector) (err) No such goal. Focus next goal with bullet ‘bullet’ (err) No such hypothesis (err), [1], [2], [3] No such hypothesis in current goal (err), [1] No such hypothesis: ‘ident’ (err), [1] No such label ‘ident’ (err) Non exhaustive pattern matching (err)

Non strictly positive occurrence of ‘ident’ in ‘type’ (err) NonCumulative (cmd) None (term) Nonrecursive Elimination Schemes (flag) not (term) Not a context variable (err) Not a discriminable equality (err) Not a primitive equality (err) Not a projectable equality but a discriminable one (err) Not a proposition or a type (err) Not a valid ring equation (err) Not a variable or hypothesis (err) Not an evar (err) Not an exact proof (err) Not an inductive goal with 1 constructor (err) Not an inductive goal with 2 constructors (err) Not an inductive product (err), [1] Not convertible (err) Not enough constructors (err) Not equal (err) Not reducible (err) Not the right number of induction arguments (err) Not the right number of missing arguments (err), [1] not_eq_S (term) Notation (cmd) Notations for lists Nothing to do, it is an equality between convertible ‘terms’ (err) Nothing to inject (err) Nothing to rewrite (err) notT (term) notypeclasses refine (tacnv) now (tacnv) nra (tacn) nsatz (tacn) nth (term)

O

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

omega: Unrecognized atomic proposition: ... (err) omega: Unrecognized predicate or connective: ‘ident’ (err) omega: Unrecognized proposition (err) once (tacn) only ... : ... (tacnv) Opaque (cmd) Open Scope (cmd) Optimize Heap (cmd) Optimize Proof (cmd) optimize_heap (tacn) option (term) or (term) or_introl (term) or_intror (term)

P

pair (term) par: ... (tacnv) Parameter (cmd) Parameters (cmdv) Parsing Explicit (flag) pattern (tacn) Peano's arithmetic plus (term) plus_n_O (term) plus_n_Sm (term) Polymorphic (cmd) Polymorphic Inductive Cumulativity (flag) pose (ssreflect) (tacn) pose (tacn) pose proof (tacnv) pred (term) pred_Sn (term) Prenex Implicits (cmd), [1] Preterm (cmd) Primitive Projections (flag) Print (cmd) Print All (cmd) Print All Dependencies (cmdv) Print Assumptions (cmd) Print Canonical Projections (cmd) Print Classes (cmd) Print Coercion Paths (cmd) Print Coercions (cmd) Print Extraction Blacklist (cmd) Print Extraction Inline (cmd) Print Firstorder Solver (cmd) Print Grammar constr (cmd) Print Grammar pattern (cmd) Print Grammar tactic (cmd) Print Graph (cmd) Print Hint (cmd), [1], [2], [3] Print HintDb (cmd) Print Implicit (cmd) Print Instances (cmd) Print Libraries (cmd) Print LoadPath (cmd) Print Ltac (cmd) Print Ltac Signatures (cmd) Print ML Modules (cmd) Print ML Path (cmd) Print Module (cmd) Print Module Type (cmd) Print Opaque Dependencies (cmdv) Print Options (cmd) Print Rewrite HintDb (cmd) Print Scope (cmdv) Print Scopes (cmd) Print Strategy (cmd) Print Table @table (cmd)

Print Tables (cmd) Print Term (cmdv) Print Transparent Dependencies (cmdv) Print Universes (cmd) Print Visibility (cmd) 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 (opt) 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 Primitive Projection Compatibility (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 Width (opt) Printing Wildcard (flag) prod (term) Program Cases (flag) Program Definition (cmd) Program Fixpoint (cmd) Program Generalized Coercion (flag) Program Instance (cmdv) Program Lemma (cmd) Programming progress (tacn) proj1 (term) proj2 (term) projT1 (term) projT2 (term) Proof (cmd) Proof `term` (cmd) Proof is not complete. (abstract) (err) Proof is not complete. (assert) (err) Proof using (cmd) Proof with (cmd) Prop Proposition (cmdv) psatz (tacn) Pwd (cmd)

Q

Qed (cmd) Quantifiers

Quit (cmd) quote (tacn) quote: not a simple fixpoint (err)

R

Record (cmd) Records declared with the keyword Record or Structure cannot be recursive (err) Recursion Recursive Extraction (cmd) Recursive Extraction Library (cmd) red (tacn) Redirect (cmd) refine (tacn) Refine Instance Mode (flag) Refine passed ill-formed term (err) refl_identity (term) reflexivity (tacn) Regular Subst Tactic (flag) Remark (cmdv) remember (tacn) Remove @table (cmd) Remove Hints (cmd) Remove LoadPath (cmd) rename (tacn) repeat (tacn) replace (tacn) Require (cmd) Require Export (cmdv) Require Import (cmdv)

Require is not allowed inside a module or a module type (err) Reset (cmd) Reset Extraction Blacklist (cmd) Reset Extraction Inline (cmd) Reset Ltac Profile (cmd) reset ltac profile (tacn) Restart (cmdv) restart_timer (tacn) rev (term) Reversible Pattern Implicit (flag) revert (tacn) revert dependent (tacnv) revgoals (tacn) rewrite (ssreflect) (tacn) rewrite (tacn) rewrite_strat (tacn) Rewriting Schemes (flag) right (tacnv) (term) ring (tacn) Ring operation should be declared as a morphism (err) ring_simplify (tacn) romega (tacnv) rtauto (tacn)

S

S (term) Save (cmdv) Scheme (cmd) Scheme Equality (cmdv) Search (cmd) Search (ssreflect) (cmd) Search Blacklist ‘string’ (table) Search Output Name Only (flag) SearchAbout (cmdv) SearchHead (cmd) SearchPattern (cmd) SearchRewrite (cmd) Section (cmd) Separate Extraction (cmd) Set (cmd) (sort) set (ssreflect) (tacn) set (tacn) Set @option (cmd) setoid_reflexivity (tacnv) setoid_replace (tacnv) setoid_rewrite (tacnv) setoid_symmetry (tacnv) setoid_transitivity (tacnv) shelve (tacn) shelve_unifiable (tacnv) Short Module Printing (flag) Show (cmd) Show Conjectures (cmdv) Show Existentials (cmdv) Show Intro (cmdv) Show Intros (cmdv) Show Ltac Profile (cmd) show ltac profile (tacn), [1] Show Obligation Tactic (cmd) Show Proof (cmdv) Show Script (cmdv) Show Universes (cmdv) Shrink Obligations (flag) sig (term) sig2 (term) Signature components for label ‘ident’ do not match (err) sigT (term)

sigT2 (term) Silent (flag) simpl (tacn) simple apply (tacnv) simple destruct (tacnv) simple eapply (tacnv) simple induction (tacnv) simple inversion (tacnv) simple notypeclasses refine (tacnv) simple refine (tacnv) simplify_eq (tacn) singel: / (term) snd (term) solve (tacn) Solve All Obligations (cmd) Solve Obligations (cmd) Some (term) specialize (tacnv) split (tacnv) split_Rabs (tacn) split_Rmult (tacn) SsrHave NoTCResolution (flag) Stable Omega (flag) start ltac profiling (tacn) Statement without assumptions (err) stepl (tacn) stepr (tacnv) stop ltac profiling (tacn) Strategy (cmd) Strict Implicit (flag) Strict Universe Declaration (flag) Strongly Strict Implicit (flag) Structural Injection (flag) Structure (cmdv) subst (tacn) suff (tacn) suffices (tacnv) Suggest Proof Using (flag) sum (term) sumbool (term) sumor (term) swap (tacn) sym_not_eq (term) symmetry (tacn)

T

Tactic Failure message (level ‘num’) (err) Tactic generated a subgoal identical to the original goal. This happens if ‘term’ does not occur in the goal (err) Tactic Notation (cmd) tail (term) tauto (tacn) Terms do not have convertible types (err) Test (cmd), [1], [2] Test @table for (cmd) The command has not failed! (err) The conclusion is not a substitutive equation (err) The conclusion of ‘type’ is not valid it must be built from ‘ident’ (err) The constructor ‘ident’ expects ‘num’ arguments (err) The elimination predicate term should be of arity ‘num’ (for non dependent case) or ‘num’ (for dependent case) (err) The file `ident.vo` contains library dirpath and not library dirpath’ (err) The recursive argument must be specified (err) The reference is not unfoldable (err) The reference ‘qualid’ was not found in the current environment (err), [1], [2] The term ‘term’ has type ‘type’ which should be Set, Prop or Type (err) The term ‘term’ has type ‘type’ while it is expected to have type ‘type’' (err) The variable ‘ident’ is already defined (err) The ‘num’ th argument of ‘ident’ must be ‘ident’ in ‘type’ (err) The ‘term’ provided does not end with an equation (err) Theorem (cmd) Theories This is not the last opened module (err) This is not the last opened module type (err) This is not the last opened section (err) This object does not support universe names (err) This proof is focused, but cannot be unfocused this way (err) This tactic has more than one success (err)

Time (cmd) time (tacn) time_constr (tacn) Timeout (cmd) timeout (tacn) Too few occurrences (err), [1] transitivity (tacn) Transparent (cmd) Transparent Obligations (flag) transparent_abstract (tacnv) trivial (tacnv) True (term) true (term) try (tacn) tryif (tacn) Trying to mask the absolute name ‘qualid’! (warn) tt (term) Type type_scope Typeclass Resolution For Conversion (flag) Typeclasses Debug (flag) Typeclasses Debug Verbosity (opt) Typeclasses Dependency Order (flag) Typeclasses eauto (cmd) typeclasses eauto (tacn) Typeclasses Filtered Unification (flag) Typeclasses Limit Intros (flag) Typeclasses Opaque (cmd) Typeclasses Strict Resolution (flag) Typeclasses Transparent (cmd) Typeclasses Unique Instances (flag) Typeclasses Unique Solutions (flag)

U

Unable to apply (err) Unable to find an instance for the variables ‘ident’ ... ‘ident’ (err) Unable to find an instance for the variables ‘ident’…‘ident’ (err) Unable to infer a match predicate (err) Unable to satisfy the rewriting constraints (err) Unable to unify ... with ... (err) Unable to unify ‘term’ with ‘term’ (err), [1] Unbound context identifier ‘ident’ (err) Undeclared universe ‘ident’ (err) Undelimit Scope (cmd) Undo (cmd) Unfocus (cmd) Unfocused (cmd)

unfold (tacn) unify (tacn) unit (term) Universal Lemma Under Conjunction (flag) Universe (cmd) Universe inconsistency (err) Universe instance should have length ‘num’ (err) Universe Minimization ToSet (flag) Universe Polymorphism (flag) Unknown inductive type (err) unlock (tacn) Unset (cmd) Unset @option (cmd) Unshelve (cmd)

V

value (term) Variable (cmd) Variable ‘ident’ is already declared (err)

Variables (cmdv) Variant (cmd) vm_compute (tacnv)

W

Warnings (opt) 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 (warn) without loss (tacnv) wlog (tacn) Wrong bullet ‘bullet’: Bullet ‘bullet’ is mandatory here (err) Wrong bullet ‘bullet’: Current bullet ‘bullet’ is not finished (err)

記号

‘class’ must be a transparent constant (err) ‘ident’ cannot be defined (warn) ‘ident’ is already used (err), [1] ‘ident’ is not a local definition (err) ‘ident’ is not an inductive type (err) ‘ident’ is used in conclusion (err) ‘ident’ is used in hypothesis ‘ident’ (err) ‘ident’ is used in the conclusion (err) ‘ident’ is used in the hypothesis ‘ident’ (err), [1]

‘ident’: no such entry (err) ‘qualid’ does not denote an evaluable constant (err) ‘qualid’ does not occur (err) ‘qualid’ does not respect the uniform inheritance condition (err) ‘qualid’ is already a coercion (err) ‘qualid’ is not a function (err) ‘qualid’ is not a module (err) ‘qualid’ not a defined object (err) ‘qualid’ not declared (err) ‘term’ cannot be used as a hint (err), [1]