Vernacular commands¶
Displaying¶

Command
Print Term? reference univ_name_list?
¶  univ_name_list
::=
@{ name* }Displays definitions of terms, including opaque terms, for the object
reference
.Term
 a syntactic marker to allow printing a term that is the same as one of the variousPrint
commands. For example,Print All
is a different command, whilePrint Term All
shows information on the object whose name is "All
".univ_name_list
 locally renames the polymorphic universes ofreference
. The name_
means the usual name is printed.

Error
This object does not support universe names.
¶

Command
Print All
¶ This command displays information about the current state of the environment, including sections and modules.
Query commands¶
Unlike other commands, query_command
s may be prefixed with
a goal selector (num:
) to specify which goal context it applies to.
If no selector is provided,
the command applies to the current goal. If no proof is open, then the command only applies
to accessible objects. (see Section Invocation of tactics).

Command
About reference univ_name_list?
¶ Displays information about the
reference
object, which, if a proof is open, may be a hypothesis of the selected goal, or an accessible theorem, axiom, etc.: its kind (module, constant, assumption, inductive, constructor, abbreviation, …), long name, type, implicit arguments and argument scopes (as set in the definition ofreference
or subsequently with theArguments
command). It does not print the body of definitions or proofs.

Command
Check term
¶ Displays the type of
term
. When called in proof mode, the term is checked in the local context of the selected goal.

Command
Eval red_expr in term
¶ Performs the specified reduction on
term
and displays the resulting term with its type. If a proof is open,term
may reference hypotheses of the selected goal.See also
Section Performing computations.

Command
Compute term
¶ Evaluates
term
using the bytecodebased virtual machine. It is a shortcut forEval
vm_compute in term
.See also
Section Performing computations.

Command
Search search_query+ insideoutside qualid+?
¶ This command can be used to filter the goal and the global context to retrieve objects whose name or type satisfies a number of conditions. Library files that were not loaded with
Require
are not considered. TheSearch Blacklist
table can also be used to exclude some things from all calls toSearch
.The output of the command is a list of qualified identifiers and their types. If the
search_querySearch Output Name Only
flag is on, the types are omitted.::=
search_item
 search_query
[ search_query++ ]Multiple
search_item
s can be combined into a complexsearch_query
: search_query
Excludes the objects that would be filtered by
search_query
. See this example.[ search_query+  ...  search_query+ ]
This is a disjunction of conjunctions of queries. A simple conjunction can be expressed by having a single disjunctive branch. For a conjunction at toplevel, the surrounding brackets are not required.
::=
headhypconclheadhypheadconcl :? string % scope_key?
headhypconclheadhypheadconcl :? one_term
is : logical_kindSearched objects can be filtered by patterns, by the constants they contain (identified by their name or a notation) and by their names. The location of the pattern or constant within a term
one_term
Search for objects whose type contains a subterm matching the pattern
one_term
. Holes of the pattern are indicated by_
or?ident
. If the same?ident
occurs more than once in the pattern, all occurrences in the subterm must be identical. See this example.string % scope_key?
If
string
is a substring of a valid identifier and no% scope_key
is provided, search for objects whose name containsstring
. See this example.Otherwise, search for objects whose type contains the reference that this string, interpreted as a notation, is attached to (as described in
reference
). See this example.
Note
To refer to a string used in a notation that is a substring of a valid identifier, put it between single quotes or explicitly provide a scope. See this example.
hyp:
The provided pattern or reference is matched against any subterm of an hypothesis of the type of the objects. See this example.
headhyp:
The provided pattern or reference is matched against the subterms in head position (any partial applicative subterm) of the hypotheses of the type of the objects. See the previous example.
concl:
The provided pattern or reference is matched against any subterm of the conclusion of the type of the objects. See this example.
headconcl:
The provided pattern or reference is matched against the subterms in head position (any partial applicative subterm) of the conclusion of the type of the objects. See the previous example.
head:
This is simply the union between
headconcl:
andheadhyp:
.is: logical_kind
 logical_kind
::=
thm_tokenassumption_token
DefinitionExampleContextPrimitive
CoercionInstanceSchemeCanonicalSubClass
FieldMethodFilters objects by the keyword that was used to define them (
Theorem
,Lemma
,Axiom
,Variable
,Context
,Primitive
...) or its status (Coercion
,Instance
,Scheme
,Canonical
,SubClass
, Field` for record fields,Method
for class fields). Note thatCoercion
s,Canonical Structure
s, Instance`s andScheme
s can be defined without using those keywords. See this example.
Additional clauses:
inside qualid+
 limit the search to the specified modulesoutside qualid+
 exclude the specified modules from the search

Error
Module/section qualid not found.
¶ There is no constant in the environment named
qualid
, wherequalid
is in aninside
oroutside
clause.
Example: Searching for a pattern
 Require Import PeanoNat.
We can repeat metavariables to narrow down the search. Here, we are looking for commutativity lemmas.
 Search (_ ?n ?m = _ ?m ?n).
 Nat.land_comm: forall a b : nat, Nat.land a b = Nat.land b a Nat.lor_comm: forall a b : nat, Nat.lor a b = Nat.lor b a Nat.lxor_comm: forall a b : nat, Nat.lxor a b = Nat.lxor b a Nat.lcm_comm: forall a b : nat, Nat.lcm a b = Nat.lcm b a Nat.min_comm: forall n m : nat, Nat.min n m = Nat.min m n Nat.gcd_comm: forall n m : nat, Nat.gcd n m = Nat.gcd m n Bool.xorb_comm: forall b b' : bool, xorb b b' = xorb b' b Nat.max_comm: forall n m : nat, Nat.max n m = Nat.max m n Nat.mul_comm: forall n m : nat, n * m = m * n Nat.add_comm: forall n m : nat, n + m = m + n Bool.orb_comm: forall b1 b2 : bool, (b1  b2)%bool = (b2  b1)%bool Bool.andb_comm: forall b1 b2 : bool, (b1 && b2)%bool = (b2 && b1)%bool Nat.eqb_sym: forall x y : nat, (x =? y) = (y =? x)
Example: Searching for part of an identifier
 Search "_assoc".
 or_assoc: forall A B C : Prop, (A \/ B) \/ C <> A \/ B \/ C and_assoc: forall A B C : Prop, (A /\ B) /\ C <> A /\ B /\ C eq_trans_assoc: forall [A : Type] [x y z t : A] (e : x = y) (e' : y = z) (e'' : z = t), eq_trans e (eq_trans e' e'') = eq_trans (eq_trans e e') e''
Example: Searching for a reference by notation
 Search "+".
 plus_O_n: forall n : nat, 0 + n = n plus_n_O: forall n : nat, n = n + 0 plus_n_Sm: forall n m : nat, S (n + m) = n + S m plus_Sn_m: forall n m : nat, S n + m = S (n + m) mult_n_Sm: forall n m : nat, n * m + n = n * S m f_equal2_plus: forall x1 y1 x2 y2 : nat, x1 = y1 > x2 = y2 > x1 + x2 = y1 + y2 nat_rect_plus: forall (n m : nat) {A : Type} (f : A > A) (x : A), nat_rect (fun _ : nat => A) x (fun _ : nat => f) (n + m) = nat_rect (fun _ : nat => A) (nat_rect (fun _ : nat => A) x (fun _ : nat => f) m) (fun _ : nat => f) n
Example: Disambiguating between part of identifier and notation
 Require Import PeanoNat.
In this example, we show two ways of searching for all the objects whose type contains
Nat.modulo
but which do not contain the substring "mod". Search "'mod'" "mod".
 Nat.bit0_eqb: forall a : nat, Nat.testbit a 0 = (a mod 2 =? 1) Nat.land_ones: forall a n : nat, Nat.land a (Nat.ones n) = a mod 2 ^ n Nat.div_exact: forall a b : nat, b <> 0 > a = b * (a / b) <> a mod b = 0 Nat.testbit_spec': forall a n : nat, Nat.b2n (Nat.testbit a n) = (a / 2 ^ n) mod 2 Nat.pow_div_l: forall a b c : nat, b <> 0 > a mod b = 0 > (a / b) ^ c = a ^ c / b ^ c Nat.testbit_eqb: forall a n : nat, Nat.testbit a n = ((a / 2 ^ n) mod 2 =? 1) Nat.testbit_false: forall a n : nat, Nat.testbit a n = false <> (a / 2 ^ n) mod 2 = 0 Nat.testbit_true: forall a n : nat, Nat.testbit a n = true <> (a / 2 ^ n) mod 2 = 1
 Search "mod"%nat "mod".
 Nat.bit0_eqb: forall a : nat, Nat.testbit a 0 = (a mod 2 =? 1) Nat.land_ones: forall a n : nat, Nat.land a (Nat.ones n) = a mod 2 ^ n Nat.div_exact: forall a b : nat, b <> 0 > a = b * (a / b) <> a mod b = 0 Nat.testbit_spec': forall a n : nat, Nat.b2n (Nat.testbit a n) = (a / 2 ^ n) mod 2 Nat.pow_div_l: forall a b c : nat, b <> 0 > a mod b = 0 > (a / b) ^ c = a ^ c / b ^ c Nat.testbit_eqb: forall a n : nat, Nat.testbit a n = ((a / 2 ^ n) mod 2 =? 1) Nat.testbit_false: forall a n : nat, Nat.testbit a n = false <> (a / 2 ^ n) mod 2 = 0 Nat.testbit_true: forall a n : nat, Nat.testbit a n = true <> (a / 2 ^ n) mod 2 = 1
Example: Search in hypotheses
The following search shows the objects whose type contains
bool
in an hypothesis as a strict subterm only: Add Search Blacklist "internal_".
 Search hyp:bool headhyp:bool.
 Nat.bitwise: (bool > bool > bool) > nat > nat > nat > nat Byte.of_bits: bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) > Byte.byte Byte.to_bits_of_bits: forall b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))), Byte.to_bits (Byte.of_bits b) = b
Example: Search in conclusion
The following search shows the objects whose type contains
bool
in the conclusion as a strict subterm only: Search concl:bool headconcl:bool.
 Byte.to_bits: Byte.byte > bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) andb_prop: forall a b : bool, (a && b)%bool = true > a = true /\ b = true andb_true_intro: forall [b1 b2 : bool], b1 = true /\ b2 = true > (b1 && b2)%bool = true Byte.to_bits_of_bits: forall b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))), Byte.to_bits (Byte.of_bits b) = b bool_choice: forall [S : Set] [R1 R2 : S > Prop], (forall x : S, {R1 x} + {R2 x}) > {f : S > bool  forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
Example: Search by keyword or status
The following search shows the definitions whose type is a
nat
or a function which returns anat
and the lemmas about+
: Search [ is:Definition headconcl:nat  is:Lemma (_ + _) ].
 Nat.two: nat Nat.zero: nat Nat.one: nat Nat.succ: nat > nat Nat.log2: nat > nat Nat.sqrt: nat > nat Nat.square: nat > nat Nat.double: nat > nat Nat.pred: nat > nat Nat.ldiff: nat > nat > nat Nat.tail_mul: nat > nat > nat Nat.land: nat > nat > nat Nat.div: nat > nat > nat Nat.modulo: nat > nat > nat Nat.lor: nat > nat > nat Nat.lxor: nat > nat > nat Nat.of_hex_uint: Hexadecimal.uint > nat Nat.of_uint: Decimal.uint > nat Nat.of_num_uint: Numeral.uint > nat length: forall [A : Type], list A > nat plus_n_O: forall n : nat, n = n + 0 plus_O_n: forall n : nat, 0 + n = n plus_n_Sm: forall n m : nat, S (n + m) = n + S m plus_Sn_m: forall n m : nat, S n + m = S (n + m) mult_n_Sm: forall n m : nat, n * m + n = n * S m
The following search shows the instances whose type includes the classes
Reflexive
orSymmetric
: Require Import Morphisms.
 Search is:Instance [ Reflexive  Symmetric ].
 iff_Symmetric: Symmetric iff iff_Reflexive: Reflexive iff impl_Reflexive: Reflexive Basics.impl eq_Symmetric: forall {A : Type}, Symmetric eq eq_Reflexive: forall {A : Type}, Reflexive eq Equivalence_Symmetric: forall {A : Type} {R : Relation_Definitions.relation A}, Equivalence R > Symmetric R Equivalence_Reflexive: forall {A : Type} {R : Relation_Definitions.relation A}, Equivalence R > Reflexive R PER_Symmetric: forall {A : Type} {R : Relation_Definitions.relation A}, PER R > Symmetric R PreOrder_Reflexive: forall {A : Type} {R : Relation_Definitions.relation A}, PreOrder R > Reflexive R reflexive_eq_dom_reflexive: forall {A B : Type} {R' : Relation_Definitions.relation B}, Reflexive R' > Reflexive (eq ==> R')%signature

Command
SearchHead one_term insideoutside qualid+?
¶ Deprecated since version 8.12: Use the
headconcl:
clause ofSearch
instead.Displays the name and type of all hypotheses of the selected goal (if any) and theorems of the current context that have the form
forall binder*,? P_{i} >* C
whereone_term
matches a subterm ofC
in head position. For example, aone_term
off _ b
matchesf a b
, which is a subterm ofC
in head position whenC
isf a b c
.See
Search
for an explanation of theinside
/outside
clauses.Example:
SearchHead
examples Add Search Blacklist "internal_".
 SearchHead le.
 Toplevel input, characters 014: > SearchHead le. > ^^^^^^^^^^^^^^ Warning: SearchHead is deprecated. Use the headconcl: clause of Search instead. [deprecatedsearchhead,deprecated] le_n: forall n : nat, n <= n le_0_n: forall n : nat, 0 <= n le_S: forall n m : nat, n <= m > n <= S m le_pred: forall n m : nat, n <= m > Nat.pred n <= Nat.pred m le_n_S: forall n m : nat, n <= m > S n <= S m le_S_n: forall n m : nat, S n <= S m > n <= m
 SearchHead (@eq bool).
 Toplevel input, characters 022: > SearchHead (@eq bool). > ^^^^^^^^^^^^^^^^^^^^^^ Warning: SearchHead is deprecated. Use the headconcl: clause of Search instead. [deprecatedsearchhead,deprecated] andb_true_intro: forall [b1 b2 : bool], b1 = true /\ b2 = true > (b1 && b2)%bool = true

Command
SearchPattern one_term insideoutside qualid+?
¶ Displays the name and type of all hypotheses of the selected goal (if any) and theorems of the current context ending with
forall binder*,? P_{i} >* C
that match the patternone_term
.See
Search
for an explanation of theinside
/outside
clauses.Example:
SearchPattern
examples Require Import Arith.
 [Loading ML file newring_plugin.cmxs ... done]
 SearchPattern (_ + _ = _ + _).
 Nat.add_comm: forall n m : nat, n + m = m + n plus_Snm_nSm: forall n m : nat, S n + m = n + S m Nat.add_succ_comm: forall n m : nat, S n + m = n + S m Nat.add_shuffle3: forall n m p : nat, n + (m + p) = m + (n + p) plus_assoc_reverse: forall n m p : nat, n + m + p = n + (m + p) Nat.add_assoc: forall n m p : nat, n + (m + p) = n + m + p Nat.add_shuffle0: forall n m p : nat, n + m + p = n + p + m f_equal2_plus: forall x1 y1 x2 y2 : nat, x1 = y1 > x2 = y2 > x1 + x2 = y1 + y2 Nat.add_shuffle2: forall n m p q : nat, n + m + (p + q) = n + q + (m + p) Nat.add_shuffle1: forall n m p q : nat, n + m + (p + q) = n + p + (m + q)
 SearchPattern (nat > bool).
 Nat.odd: nat > bool Init.Nat.odd: nat > bool Nat.even: nat > bool Init.Nat.even: nat > bool Init.Nat.testbit: nat > nat > bool Nat.leb: nat > nat > bool Nat.eqb: nat > nat > bool Init.Nat.eqb: nat > nat > bool Nat.ltb: nat > nat > bool Nat.testbit: nat > nat > bool Init.Nat.leb: nat > nat > bool Init.Nat.ltb: nat > nat > bool BinNat.N.testbit_nat: BinNums.N > nat > bool BinPosDef.Pos.testbit_nat: BinNums.positive > nat > bool BinPos.Pos.testbit_nat: BinNums.positive > nat > bool BinNatDef.N.testbit_nat: BinNums.N > nat > bool
 SearchPattern (forall l : list _, _ l l).
 List.incl_refl: forall [A : Type] (l : list A), List.incl l l List.lel_refl: forall [A : Type] (l : list A), List.lel l l
 SearchPattern (?X1 + _ = _ + ?X1).
 Nat.add_comm: forall n m : nat, n + m = m + n

Command
SearchRewrite one_term insideoutside qualid+?
¶ Displays the name and type of all hypotheses of the selected goal (if any) and theorems of the current context that have the form
forall binder*,? P_{i} >* LHS = RHS
whereone_term
matches eitherLHS
orRHS
.See
Search
for an explanation of theinside
/outside
clauses.Example:
SearchRewrite
examples Require Import Arith.
 SearchRewrite (_ + _ + _).
 Nat.add_shuffle0: forall n m p : nat, n + m + p = n + p + m plus_assoc_reverse: forall n m p : nat, n + m + p = n + (m + p) Nat.add_assoc: forall n m p : nat, n + (m + p) = n + m + p Nat.add_shuffle1: forall n m p q : nat, n + m + (p + q) = n + p + (m + q) Nat.add_shuffle2: forall n m p q : nat, n + m + (p + q) = n + q + (m + p) Nat.add_carry_div2: forall (a b : nat) (c0 : bool), (a + b + Nat.b2n c0) / 2 = a / 2 + b / 2 + Nat.b2n (Nat.testbit a 0 && Nat.testbit b 0  c0 && (Nat.testbit a 0  Nat.testbit b 0))

Table
Search Blacklist string
¶ Specifies a set of strings used to exclude lemmas from the results of
Search
,SearchHead
,SearchPattern
andSearchRewrite
queries. A lemma whose fullyqualified name contains any of the strings will be excluded from the search results. The default blacklisted substrings are_subterm
,_subproof
andPrivate_
.Use the
Add
andRemove
commands to update the set of blacklisted strings.

Flag
Search Output Name Only
¶ This flag restricts the output of search commands to identifier names; turning it on causes invocations of
Search
,SearchHead
,SearchPattern
,SearchRewrite
etc. to omit types from their output, printing only identifiers.
Requests to the environment¶

Command
Print Assumptions reference
¶ Displays all the assumptions (axioms, parameters and variables) a theorem or definition depends on.
The message "Closed under the global context" indicates that the theorem or definition has no dependencies.

Command
Print Opaque Dependencies reference
¶ Displays the assumptions and opaque constants that
reference
depends on.

Command
Print Transparent Dependencies reference
¶ Displays the assumptions and transparent constants that
reference
depends on.

Command
Print All Dependencies reference
¶ Displays all the assumptions and constants
reference
depends on.

Command
Locate reference
¶  reference
::=
qualid
string % scope_key?Displays the full name of objects from Coq's various qualified namespaces such as terms, modules and Ltac, thereby showing the module they are defined in. It also displays notation definitions.
qualid
refers to object names that end with
qualid
.string % scope_key?
refers to definitions of notations.
string
can be a single token in the notation such as ">
" or a pattern that matches the notation. See Locating notations.% scope_key
, if present, limits the reference to the scope bound to the delimiting keyscope_key
, such as, for example,%nat
. (see Section Local interpretation rules for notations)

Command
Locate Library qualid
¶ Displays the full name, status and file system path of the module
qualid
, whether loaded or not.

Command
Locate File string
¶ Displays the file system path of the file ending with
string
. Typically,string
has a suffix such as.cmo
or.vo
or.v
file, such asNat.v
.
Example: Locate examples
 Locate nat.
 Inductive Coq.Init.Datatypes.nat
 Locate Datatypes.O.
 Constructor Coq.Init.Datatypes.O (shorter name to refer to it in current context is O)
 Locate Init.Datatypes.O.
 Constructor Coq.Init.Datatypes.O (shorter name to refer to it in current context is O)
 Locate Coq.Init.Datatypes.O.
 Constructor Coq.Init.Datatypes.O (shorter name to refer to it in current context is O)
 Locate I.Dont.Exist.
 No object of suffix I.Dont.Exist
Printing flags¶

Flag
Fast Name Printing
¶ When turned on, Coq uses an asymptotically faster algorithm for the generation of unambiguous names of bound variables while printing terms. While faster, it is also less clever and results in a typically less elegant display, e.g. it will generate more names rather than reusing certain names across subterms. This flag is not enabled by default, because as Ltac observes bound names, turning it on can break existing proof scripts.
Loading files¶
Coq offers the possibility of loading different parts of a whole development stored in separate files. Their contents will be loaded as if they were entered from the keyboard. This means that the loaded files are text files containing sequences of commands for Coq’s toplevel. This kind of file is called a script for Coq. The standard (and default) extension of Coq’s script files is .v.

Command
Load Verbose? stringident
¶ Loads a file. If
ident
is specified, the command loads a file namedident.v
, searching successively in each of the directories specified in the loadpath. (see Section Libraries and filesystem)If
string
is specified, it must specify a complete filename.~
and .. abbreviations are allowed as well as shell variables. If no extension is specified, Coq will use the default extension.v
.Files loaded this way can't leave proofs open, nor can
Load
be used inside a proof.We discourage the use of
Load
; useRequire
instead.Require
loads.vo
files that were previously compiled from.v
files.Verbose
displays the Coq output for each command and tactic in the loaded file, as if the commands and tactics were entered interactively.
Error
Load is not supported inside proofs.
¶

Error
Files processed by Load cannot leave open proofs.
¶

Error
Compiled files¶
This section describes the commands used to load compiled files (see Chapter The Coq commands for documentation on how to compile a file). A compiled file is a particular case of a module called a library file.

Command
Require ImportExport? qualid+
¶ Loads compiled modules into the Coq environment. For each
qualid
, which has the formident_{prefix} .* ident
, the command searches for the logical name represented by theident_{prefix}
s and loads the compiled fileident.vo
from the associated filesystem directory.The process is applied recursively to all the loaded files; if they contain
Require
commands, those commands are executed as well. The compiled files must have been compiled with the same version of Coq. The compiled files are neither replayed nor rechecked.Import
 additionally does anImport
on the loaded module, making components defined in the module available by their short namesExport
 additionally does anExport
on the loaded module, making components defined in the module available by their short names and marking them to be exported by the current module
If the required module has already been loaded,
Import
andExport
make the command equivalent toImport
orExport
.The loadpath must contain the same mapping used to compile the file (see Section Libraries and filesystem). If several files match, one of them is picked in an unspecified fashion. Therefore, library authors should use a unique name for each module and users are encouraged to use fullyqualified names or the
From … Require
command to load files.
Command
From dirpath Require ImportExport? qualid+
¶ Works like
Require
, but loads, for eachqualid
, the library whose fullyqualified name matchesdirpath.ident .*qualid
for someident .*
. This is useful to ensure that thequalid
library comes from a particular package.

Error
Cannot find library foo in loadpath.
¶ The command did not find the file foo.vo. Either foo.v exists but is not compiled or foo.vo is in a directory which is not in your LoadPath (see Section Libraries and filesystem).

Error
Compiled library ident.vo makes inconsistent assumptions over library qualid.
¶ The command tried to load library file
ident
.vo that depends on some specific version of libraryqualid
which is not the one already loaded in the current Coq session. Probablyident.v
was not properly recompiled with the last version of the file containing modulequalid
.

Error
Bad magic number.
¶ The file
ident.vo
was found but either it is not a Coq compiled module, or it was compiled with an incompatible version of Coq.

Error
The file ident.vo contains library qualid_{1} and not library qualid_{2}.
¶ The library
qualid_{2}
is indirectly required by aRequire
orFrom … Require
command. The loadpath mapsqualid_{2}
toident.vo
, which was compiled using a loadpath that bound it toqualid_{1}
. Usually the appropriate solution is to recompileident.v
using the correct loadpath. See Libraries and filesystem.

Warning
Require inside a module is deprecated and strongly discouraged. You can Require a module at toplevel and optionally Import it inside another one.
¶ Note that the
Import
andExport
commands can be used inside modules.See also
Chapter The Coq commands

Command
Print Libraries
¶ This command displays the list of library files loaded in the current Coq session.

Command
Declare ML Module string+
¶ This commands dynamically loads OCaml compiled code from a
.mllib
file. It is used to load plugins dynamically. The files must be accessible in the current OCaml loadpath (see the commandAdd ML Path
). The.mllib
suffix may be omitted.This command is reserved for plugin developers, who should provide a .v file containing the command. Users of the plugins will then generally load the .v file.
This command supports the
local
attribute. If present, the listed files are not exported, even if they're outside a section.

Command
Print ML Modules
¶ This prints the name of all OCaml modules loaded with
Declare ML Module
. To know from where these module were loaded, the user should use the commandLocate File
.
Loadpath¶
Loadpaths are preferably managed using Coq command line options (see Section Libraries and filesystem) but there remain vernacular commands to manage them for practical purposes. Such commands are only meant to be issued in the toplevel, and using them in source files is discouraged.

Command
Pwd
¶ This command displays the current working directory.

Command
Cd string?
¶ If
string
is specified, changes the current directory according tostring
which can be any valid path. Otherwise, it displays the current directory.

Command
Add LoadPath string as dirpath
¶  dirpath
::=
ident .* identThis command is equivalent to the command line option
Q string dirpath
. It adds a mapping to the loadpath from the logical namedirpath
to the file system directorystring
.

Command
Add Rec LoadPath string as dirpath
¶ This command is equivalent to the command line option
R string dirpath
. It adds the physical directory string and all its subdirectories to the current Coq loadpath.

Command
Print LoadPath dirpath?
¶ This command displays the current Coq loadpath. If
dirpath
is specified, displays only the paths that extend that prefix.

Command
Add ML Path string
¶ This command adds the path
string
to the current OCaml loadpath (cf.Declare ML Module
).

Command
Print ML Path
¶ This command displays the current OCaml loadpath. This command makes sense only under the bytecode version of
coqtop
, i.e. using optionbyte
(cf.Declare ML Module
).
Backtracking¶
The backtracking commands described in this section can only be used
interactively, they cannot be part of a vernacular file loaded via
Load
or compiled by coqc
.

Command
Reset ident
¶ This command removes all the objects in the environment since
ident
was introduced, includingident
.ident
may be the name of a defined or declared object as well as the name of a section. One cannot reset over the name of a module or of an object inside a module.

Command
Reset Initial
¶ Goes back to the initial state, just after the start of the interactive session.

Command
Back num?
¶ Undoes all the effects of the last
num sentence
s. Ifnum
is not specified, the command undoes one sentence. Sentences read from a.v
file via aLoad
are considered a single sentence. WhileBack
can undo tactics and commands executed within proof mode, once you exit proof mode, such as withQed
, all the statements executed within are thereafter considered a single sentence.Back
immediately followingQed
gets you back to the state just after the statement of the proof.
Error
Invalid backtrack.
¶ The user wants to undo more commands than available in the history.

Error

Command
BackTo num
¶ This command brings back the system to the state labeled
num
, forgetting the effect of all commands executed after this state. The state label is an integer which grows after each successful command. It is displayed in the prompt when in emacs mode. Just asBack
(see above), theBackTo
command now handles proof states. For that, it may have to undo some extra commands and end on a statenum′ ≤ num
if necessary.
Quitting and debugging¶

Command
Quit
¶ Causes Coq to exit. Valid only in coqtop.

Command
Drop
¶ This command temporarily enters the OCaml toplevel. It is a debug facility used by Coq’s implementers. Valid only in the bytecode version of coqtop. The OCaml command:
#use "include";;
adds the right loadpaths and loads some toplevel printers for all abstract types of Coq section_path, identifiers, terms, judgments, …. You can also use the file base_include instead, that loads only the prettyprinters for section_paths and identifiers. You can return back to Coq with the command:
go();;
Warning
It only works with the bytecode version of Coq (i.e.
coqtop.byte
, see Sectioninteractiveuse
).You must have compiled Coq from the source package and set the environment variable COQTOP to the root of your copy of the sources (see Section
customizationbyenvironmentvariables
).

Command
Redirect string sentence
¶ Executes
sentence
, redirecting its output to the file "string
.out".

Command
Timeout num sentence
¶ Executes
sentence
. If the operation has not terminated afternum
seconds, then it is interrupted and an error message is displayed.

Command
Fail sentence
¶ For debugging scripts, sometimes it is desirable to know whether a command or a tactic fails. If
sentence
fails, thenFail sentence
succeeds (except for critical errors, such as "stack overflow"), without changing the proof state. In interactive mode, the system prints a message confirming the failure.
Note
Time
, Redirect
, Timeout
and Fail
are
control_command
s. For these commands, attributes and goal
selectors, when specified, are part of the sentence
argument, and thus come after
the control command prefix and before the inner command or tactic. For
example: Time #[ local ] Definition foo := 0.
or Fail Timeout 10 all: auto.
Controlling display¶

Flag
Silent
¶ This flag controls the normal displaying.

Option
Warnings "+? ident+,"
¶ This option configures the display of warnings. It is experimental, and expects, between quotes, a commaseparated list of warning names or categories. Adding  in front of a warning or category disables it, adding + makes it an error. It is possible to use the special categories all and default, the latter containing the warnings enabled by default. The flags are interpreted from left to right, so in case of an overlap, the flags on the right have higher priority, meaning that
A,A
is equivalent toA
.

Option
Printing Width num
¶ This command sets which leftaligned part of the width of the screen is used for display. At the time of writing this documentation, the default value is 78.

Option
Printing Depth num
¶ This option controls the nesting depth of the formatter used for pretty printing. Beyond this depth, display of subterms is replaced by dots. At the time of writing this documentation, the default value is 50.

Flag
Printing Compact Contexts
¶ This flag controls the compact display mode for goals contexts. When on, the printer tries to reduce the vertical size of goals contexts by putting several variables (even if of different types) on the same line provided it does not exceed the printing width (see
Printing Width
). At the time of writing this documentation, it is off by default.

Flag
Printing Unfocused
¶ This flag controls whether unfocused goals are displayed. Such goals are created by focusing other goals with bullets (see Bullets or curly braces). It is off by default.

Flag
Printing Dependent Evars Line
¶ This flag controls the printing of the “(dependent evars: …)” information after each tactic. The information is used by the Prooftree tool in Proof General. (https://askra.de/software/prooftree)
Printing constructions in full¶

Flag
Printing All
¶ Coercions, implicit arguments, the type of pattern matching, but also notations (see Syntax extensions and notation scopes) can obfuscate the behavior of some tactics (typically the tactics applying to occurrences of subterms are sensitive to the implicit arguments). Turning this flag on deactivates all highlevel printing features such as coercions, implicit arguments, returned type of pattern matching, notations and various syntactic sugar for pattern matching or record projections. Otherwise said,
Printing All
includes the effects of the flagsPrinting Implicit
,Printing Coercions
,Printing Synth
,Printing Projections
, andPrinting Notations
. To reactivate the highlevel printing features, use the commandUnset Printing All
.Note
In some cases, setting
Printing All
may display terms that are so big they become very hard to read. One technique to work around this is useUndelimit Scope
and/orClose Scope
to turn off the printing of notations bound to particular scope(s). This can be useful when notations in a given scope are getting in the way of understanding a goal, but turning off all notations withPrinting All
would make the goal unreadable.
Controlling the reduction strategies and the conversion algorithm¶
Coq provides reduction strategies that the tactics can invoke and two different algorithms to check the convertibility of types. The first conversion algorithm lazily compares applicative terms while the other is a bruteforce but efficient algorithm that first normalizes the terms before comparing them. The second algorithm is based on a bytecode representation of terms similar to the bytecode representation used in the ZINC virtual machine [Ler90]. It is especially useful for intensive computation of algebraic values, such as numbers, and for reflectionbased tactics. The commands to fine tune the reduction strategies and the lazy conversion algorithm are described first.

Command
Opaque reference+
¶ This command accepts the
global
attribute. By default, the scope ofOpaque
is limited to the current section or module.This command has an effect on unfoldable constants, i.e. on constants defined by
Definition
orLet
(with an explicit body), or by a command assimilated to a definition such asFixpoint
,Program Definition
, etc, or by a proof ended byDefined
. The command tells not to unfold the constants in thereference
sequence in tactics using δconversion (unfolding a constant is replacing it by its definition).Opaque
has also an effect on the conversion algorithm of Coq, telling it to delay the unfolding of a constant as much as possible when Coq has to check the conversion (see Section Conversion rules) of two distinct applied constants.See also
Sections Performing computations, Automating, Entering and leaving proof editing mode

Command
Transparent reference+
¶ This command accepts the
global
attribute. By default, the scope ofTransparent
is limited to the current section or module.This command is the converse of
Opaque
and it applies on unfoldable constants to restore their unfoldability after an Opaque command.Note in particular that constants defined by a proof ended by Qed are not unfoldable and Transparent has no effect on them. This is to keep with the usual mathematical practice of proof irrelevance: what matters in a mathematical development is the sequence of lemma statements, not their actual proofs. This distinguishes lemmas from the usual defined constants, whose actual values are of course relevant in general.

Error
The reference qualid was not found in the current environment.
¶ There is no constant named
qualid
in the environment.See also
Sections Performing computations, Automating, Entering and leaving proof editing mode

Error

Command
Strategy strategy_level [ reference+ ]+
¶  strategy_level
::=
opaque
int
expand
transparentstrategy_level_or_var::=
strategy_level
identThis command accepts the
local
attribute, which limits its effect to the current section or module, in which case the section and module behavior is the same asOpaque
andTransparent
(withoutglobal
).This command generalizes the behavior of the
Opaque
andTransparent
commands. It is used to finetune the strategy for unfolding constants, both at the tactic level and at the kernel level. This command associates astrategy_level
with the qualified names in thereference
sequence. Whenever two expressions with two distinct head constants are compared (for instance, this comparison can be triggered by a type cast), the one with lower level is expanded first. In case of a tie, the second one (appearing in the cast type) is expanded.Levels can be one of the following (higher to lower):
opaque
: level of opaque constants. They cannot be expanded by tactics (behaves like +∞, see next item).int
: levels indexed by an integer. Level 0 corresponds to the default behavior, which corresponds to transparent constants. This level can also be referred to astransparent
. Negative levels correspond to constants to be expanded before normal transparent constants, while positive levels correspond to constants to be expanded after normal transparent constants.expand
: level of constants that should be expanded first (behaves like −∞)transparent
: Equivalent to level 0

Command
Print Strategy reference
¶ This command prints the strategy currently associated with
reference
. It fails ifreference
is not an unfoldable reference, that is, neither a variable nor a constant.
Error
The reference is not unfoldable.
¶

Error

Command
Print Strategies
¶ Print all the currently nontransparent strategies.

Command
Declare Reduction ident := red_expr
¶ Declares a short name for the reduction expression
red_expr
, for instancelazy beta delta [foo bar]
. This short name can then be used inEval ident in
oreval
constructs. This command accepts thelocal
attribute, which indicates that the reduction will be discarded at the end of the file or module. The name is not qualified. In particular declaring the same name in several modules or in several functor applications will be rejected if these declarations are not local. The nameident
cannot be used directly as an Ltac tactic, but nothing prevents the user from also performing aLtac ident := red_expr
.See also
Controlling the locality of commands¶

Attribute
global
¶ 
Attribute
local
¶ Some commands support a
local
orglobal
attribute to control the scope of their effect. There is also a legacy (and much more commonly used) syntax using theLocal
orGlobal
prefixes (seelegacy_attr
). There are four kinds of commands:Commands whose default is to extend their effect both outside the section and the module or library file they occur in. For these commands, the
local
attribute limits the effect of the command to the current section or module it occurs in. As an example, theCoercion
andStrategy
commands belong to this category.Commands whose default behavior is to stop their effect at the end of the section they occur in but to extend their effect outside the module or library file they occur in. For these commands, the
local
attribute limits the effect of the command to the current module if the command does not occur in a section and theglobal
attribute extends the effect outside the current sections and current module if the command occurs in a section. As an example, theArguments
,Ltac
orNotation
commands belong to this category. Notice that a subclass of these commands do not support extension of their scope outside sections at all and theglobal
attribute is not applicable to them.Commands whose default behavior is to stop their effect at the end of the section or module they occur in. For these commands, the
global
attribute extends their effect outside the sections and modules they occur in. TheTransparent
andOpaque
commands belong to this category.Commands whose default behavior is to extend their effect outside sections but not outside modules when they occur in a section and to extend their effect outside the module or library file they occur in when no section contains them. For these commands, the
local
attribute limits the effect to the current section or module while theglobal
attribute extends the effect outside the module even when the command occurs in a section. TheSet
andUnset
commands belong to this category.
Controlling Typing Flags¶

Flag
Guard Checking
¶ This flag can be used to enable/disable the guard checking of fixpoints. Warning: this can break the consistency of the system, use at your own risk. Decreasing argument can still be specified: the decrease is not checked anymore but it still affects the reduction of the term. Unchecked fixpoints are printed by
Print Assumptions
.

Flag
Positivity Checking
¶ This flag can be used to enable/disable the positivity checking of inductive types and the productivity checking of coinductive types. Warning: this can break the consistency of the system, use at your own risk. Unchecked (co)inductive types are printed by
Print Assumptions
.

Flag
Universe Checking
¶ This flag can be used to enable/disable the checking of universes, providing a form of "type in type". Warning: this breaks the consistency of the system, use at your own risk. Constants relying on "type in type" are printed by
Print Assumptions
. It has the same effect astypeintype
command line argument (see By command line options).

Command
Print Typing Flags
¶ Print the status of the three typing flags: guard checking, positivity checking and universe checking.
See also Cumulative StrictProp
in the \(\SProp\) chapter.
Example
 Unset Guard Checking.
 Print Typing Flags.
 check_guarded: false check_positive: true check_universes: true cumulative sprop: false definitional uip: false
 Fixpoint f (n : nat) : False := f n.
 f is defined f is recursively defined (guarded on 1st argument)
 Fixpoint ackermann (m n : nat) {struct m} : nat := match m with  0 => S n  S m => match n with  0 => ackermann m 1  S n => ackermann m (ackermann (S m) n) end end.
 ackermann is defined ackermann is recursively defined (guarded on 1st argument)
 Print Assumptions ackermann.
 Axioms: ackermann is assumed to be guarded.
Note that the proper way to define the Ackermann function is to use an inner fixpoint:
 Fixpoint ack m := fix ackm n := match m with  0 => S n  S m' => match n with  0 => ack m' 1  S n' => ack m' (ackm n') end end.
 ack is defined ack is recursively defined (guarded on 1st argument)
Internal registration commands¶
Due to their internal nature, the commands that are presented in this section are not for general use. They are meant to appear only in standard libraries and in support libraries of plugins.
Exposing constants to OCaml libraries¶

Command
Register qualid_{1} as qualid_{2}
¶ Makes the constant
qualid_{1}
accessible to OCaml libraries under the namequalid_{2}
. The constant can then be dynamically located in OCaml code by callingCoqlib.lib_ref "qualid_{2}"
. The OCaml code doesn't need to know where the constant is defined (what file, module, library, etc.).As a special case, when the first segment of
qualid_{2}
iskernel
, the constant is exposed to the kernel. For instance, theInt63
module features the following declaration:Register bool as kernel.ind_bool.This makes the kernel aware of the
bool
type, which is used, for example, to define the return type of the#int63_eq
primitive.See also
Inlining hints for the fast reduction machines¶
Registering primitive operations¶

Command
Primitive ident : term? := #ident_{prim}
¶ Makes the primitive type or primitive operator
#ident_{prim}
defined in OCaml accessible in Coq commands and tactics. For internal use by implementors of Coq's standard library or standard library replacements. No space is allowed after the#
. Invalid values give a syntax error.For example, the standard library files
Int63.v
andPrimFloat.v
usePrimitive
to support, respectively, the features described in Primitive Integers and Primitive Floats.The types associated with an operator must be declared to the kernel before declaring operations that use the type. Do this with
Primitive
for primitive types andRegister
with thekernel
prefix for other types. For example, inInt63.v
,#int63_type
must be declared before the associated operations.