Commands ¶

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 of reference or subsequently with the Arguments command). It does not print the body of definitions or proofs.

Displays the type of term . When called in proof mode, the term is checked in the local context of the selected goal (possibly by using single numbered goal selectors ). This command tries to resolve existential variables as much as possible.

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. The Search Blacklist table can also be used to exclude some things from all calls to Search .

Excludes the objects that would be filtered by search_query . See this example .

This is a disjunction of conjunctions of queries. A simple conjunction can be expressed by having a single disjunctive branch. For a conjunction at top-level, the surrounding brackets are not required.

Search for objects whose type contains a subterm matching the pattern one_pattern . 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 .

If string is a substring of a valid identifier and no % scope_key is provided, search for objects whose name contains string . 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 .

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: and headhyp: .

is: logical_kind

logical_kind ::= thm_token ​ assumption_token | Definition ​ Example ​ Context ​ Primitive | Coercion ​ Instance ​ Scheme ​ Canonical ​ SubClass | Field ​ Method

Filters 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 that Coercion s, Canonical Structure s, Instance`s and Scheme s can be defined without using those keywords. See this example .

Additional clauses:

inside ​ in qualid + - limit the search to the specified modules

outside qualid + - exclude the specified modules from the search

Error Module/section qualid not found. ¶

There is no constant in the environment named qualid , where qualid is in an inside or outside clause.

Example: Searching for a pattern

Require Import PeanoNat .

We can repeat meta-variables 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)

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''

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

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.Div0.div_exact: forall a b : nat, a = b * (a / b) <-> a mod b = 0 Nat.land_ones: forall a n : nat, Nat . land a ( Nat . ones n) = a mod 2 ^ n 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.Div0.div_exact: forall a b : nat, a = b * (a / b) <-> a mod b = 0 Nat.land_ones: forall a n : nat, Nat . land a ( Nat . ones n) = a mod 2 ^ n 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 a nat 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: Number . 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 or Symmetric :

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 SearchPattern one_pattern inside ​ in ​ outside 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 pattern one_pattern .

See Search for an explanation of the inside / in / outside clauses.

Example: SearchPattern examples

Require Import Arith .

[Loading ML file ring_plugin.cmxs (using legacy method) ... done]

Search Pattern ( _ + _ = _ + _ ).

Nat.add_comm: forall n m : nat, n + m = m + n Plus.plus_Snm_nSm_stt: 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) Arith_prebase.plus_assoc_reverse_stt: 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)

Search Pattern ( 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

Search Pattern ( 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

Search Pattern (? X1 + _ = _ + ? X1 ).

Nat.add_comm: forall n m : nat, n + m = m + n Command SearchRewrite one_pattern inside ​ in ​ outside 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 where one_pattern matches either LHS or RHS .

See Search for an explanation of the inside / in / outside clauses.

Example: SearchRewrite examples

Require Import Arith .

SearchRewrite ( _ + _ + _ ).

Nat.add_shuffle0: forall n m p : nat, n + m + p = n + p + m Arith_prebase.plus_assoc_reverse_stt: 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 ¶

This table specifies a set of strings used to exclude lemmas from the results of Search , SearchPattern and SearchRewrite queries. A lemma whose fully qualified name contains any of the strings will be excluded from the search results. The default blacklisted substrings are _subterm , _subproof and Private_ .

Use the Add and Remove 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 , SearchPattern , SearchRewrite etc. to omit types from their output, printing only identifiers.

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 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.

Note that objects are reported only when the module containing them has been loaded, such as through a Require command. Notation definitions are reported only when the containing module has been imported (e.g. with Require Import or Import ).

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 key scope_key , such as, for example, %nat . (see Section Local interpretation rules for notations )

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 as Nat.v .

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 Flag Fast Name Printing ¶

When this flag is 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 ? string ​ ident ¶

Loads a file. If ident is specified, the command loads a file named ident .v , searching successively in each of the directories specified in the load path . (see Section Logical paths and the load path )

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 ; use Require 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 Can’t find file ident on loadpath. ¶

Compiled files ¶

This section describes the commands used to load compiled files (see Chapter 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 From dirpath ? Require Import ​ Export import_categories ? ? filtered_import + ¶

Loads compiled files into the Coq environment. For the first qualid in each filtered_import , the command looks in the load path for a compiled file ident .vo whose logical name has the form dirpath . ident implicit . * qualid (if From dirpath is given) or ident implicit . * qualid (if the optional From clause is absent). ident implicit . * represents the parts of the fully qualified name that are implicit. For example, From Coq Require Nat loads Coq.Init.Nat and Init is implicit. ident is the final component of the qualid .

If a file is found, its logical name must be the same as the one used to compile the file. Then the file is loaded as well as all the files it depends on (recursively). All the files must have been compiled with the same version of Coq.

Import - additionally does an Import on the loaded module, making components defined in the module available by their short names

Export - additionally does an Export 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 file has already been loaded, it is not reloaded. If Import or Export are present, the command also does the equivalent of the Import or Export commands.

A single file can be loaded with several variations of the Require command. For example, the -Q path Lib command line parameter associates the file path/Foo/File.vo with the logical name Lib.Foo.File . It allows this file to be loaded through Require Lib.Foo.File , From Lib Require Foo.File , From Lib Require File or From Lib.Foo Require File . The -R path Lib command line parameter allows loading the file with the additional alternatives Require Foo.File and Require File In particular, From is useful to ensure that the file comes from a particular package or subpackage. Use of -Q is better for avoiding ambiguous path names.

Exact matches are preferred when looking for a file with the logical name dirpath . ident implicit . * qualid or ident implicit . * qualid (that is, matches where the implicit part is empty). If the name exactly matches in multiple -R or -Q options, the file corresponding to the last -R or -Q specified is used. (In Print LoadPath , that's the first match from the top.)

If there is no exact match, the matches from the last -R or -Q are selected. If this results in a unique match, the corresponding file is selected. If this results in several matches, it is an error. The difference between the -R and the -Q option is that non-exact matches are allowed for -Q only if From is present. Matching is done when the script is compiled or processed rather than when its .vo file is loaded. .vo files use fully-qualified names.

We recommend you use -R only to refer to files in the same package. Use -Q (if necessary) to refer to files in a different package.

Error Cannot load qualid : no physical path bound to dirpath . ¶ 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 load path .

Error Required library qualid matches several files in path (found file 1 .vo, file 2 .vo, ...). ¶

The file to load must be required with a more discriminating suffix, or, at worst, with its full logical name.

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 library qualid which is not the one already loaded in the current Coq session. Probably ident .v was not properly recompiled with the last version of the file containing module qualid .

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 a Require . The load path maps qualid 2 to ident .vo , which was compiled using a load path that bound it to qualid 1 . Usually the appropriate solution is to recompile ident .v using the correct load path .

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 and Export commands can be used inside modules.

See also

Chapter Coq commands

Command Declare ML Module string + ¶

Loads an OCaml plugin and its dependencies dynamically. The string argument must be a valid findlib plugin name, for example coq-core.plugins.ltac . As of Coq 8.16, the command also supports a legacy syntax compatible with the plugin loading system used in Coq 8.0-8.15, see below.

The first component of the plugin name is a package name that has to be in scope of findlib 's' search path. One can see the paths explored by findlib by running ocamlfind printconf and get the list of available libraries by running ocamlfind list | grep coq (Coq libraries are typically named coq-something ).

This command is reserved for plugin developers, who should provide a .v file containing the command. Users of the plugin will usually require the resulting .vo file which will then transitively load the required plugin.

If you are writing a plugin, you thus need to generate the right metadata so findlib can locate your plugin. This usually involves generating some kind of META file and placing it in a place where findlib can see it. Different build systems provide different helpers to do this: see here for coq_makefile , and here for Dune .

Note that the plugin loading system for Coq changed in 8.16 to use findlib. Previous Coq versions loaded OCaml dynamic objects by first locating the object file from -I directives, then directly invoking Dynlink.loadfile . For compatibility purposes, 8.16 still supports this legacy method, with the syntax being Declare ML Module "my_package_plugin:pkg.plugin.my-package". , where my_package_plugin is the name of the OCaml object file.

This is useful if you are still using a third party build system such as Dune or your own.

This command supports the local attribute. If present, the listed files are not exported, even if they're outside a section.

Error File not found on loadpath: string . ¶

findlib is not able to find the plugin name. Possible reasons

The plugin does not exist or is misspelled. You can get the list of available libraries by running ocamlfind list | grep coq .

The metadata for findlib has not been set properly (see above).

Error Dynlink error: execution of module initializers in the ¶ Error shared library failed: Coq Error: string is not a valid ¶ Error plugin name anymore. Plugins should be loaded using their ¶ Error public name according to findlib, for example ¶ Error package-name.foo and not foo _ plugin. ¶

The plugin declaration in some .mlg file does not match the findlib plugin name. In the example of coq-core.plugins.ltac , one has to write DECLARE PLUGIN "coq-core.plugins.ltac" .

Load paths ¶

Load paths are preferably managed using Coq command line options (see Section Logical paths and the load path ), but there are also commands to manage them within Coq. These 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 to string which can be any valid path. Otherwise, it displays the current directory.

Command Add LoadPath string as dirpath ¶

Deprecated since version 8.16: Use command line -Q or -R or put them in your _CoqProject file instead.

If this command is an important feature for you, please open an issue at https://github.com/coq/coq/issues and explain your workflow.

dirpath ::= ident . * ident

This command is equivalent to the command line option -Q string dirpath . It adds a mapping to the load path from the logical name dirpath to the file system directory string .

dirpath is a prefix of a module name. The module name hierarchy follows the file system hierarchy. On Linux, for example, the prefix A.B.C maps to the directory string /B/C . Avoid using spaces after a . in the path because the parser will interpret that as the end of a command or tactic.

This command is equivalent to the command line option -R string dirpath . It adds the directory specified by the string ` and all its subdirectories to the current Coq load path .

Command Print LoadPath dirpath ? ¶

Displays the current Coq load path . If dirpath is specified, displays only the paths that extend that prefix. In the output, the logical path <> represents an empty logical path.

Command Add ML Path string ¶

Equivalent to the command line option -I string . Adds the path string to the current OCaml loadpath (cf. Declare ML Module ). It is for convenience, such as for use in an interactive session, and it is not exported to compiled files. For separation of concerns with respect to the relocability of files, we recommend using -I string .

Command Print ML Path ¶

Displays the current OCaml loadpath, as provided by the command line option -I string or by the command Add ML Path @string (cf. Declare ML Module ).

Extra Dependencies ¶

Dependencies on external files, i.e. non .v files, can be declared as follows:

Command From dirpath Extra Dependency string as ident ? ¶

Adds an additional dependency of the current .v file on an external file. This information is included in the coqdep tool generated list of dependencies. The file name string must exist relative to one of the top directories associated with dirpath . string can include directory separators ( / ) to select a file in a subdirectory. Path elements in string must be valid Coq identifiers, e.g. they cannot contain characters such as - or , . See Lexical conventions .

When ident is provided, that name can be used by OCaml code, typically in a plugin, to access the full path of the external file via the API ComExtraDeps.query_extra_dep .

This command has been available through the Comments command, e.g. Comments From … Dependency … . The Comments form is deprecated in Coq 8.16.

Warning File ... found twice in ... ¶

The file is found in more than once in the top directories associated with the given dirpath . In this case the first occurrence is selected.

Backtracking ¶

The backtracking commands described in this section can only be used interactively, they cannot be part of a Coq file loaded via Load or compiled by coqc .

Command Reset ident ¶

This command removes all the objects in the environment since ident was introduced, including ident . 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 Back natural ? ¶

Undoes all the effects of the last natural sentence s. If natural is not specified, the command undoes one sentence. Sentences read from a .v file via a Load are considered a single sentence. While Back can undo tactics and commands executed within proof mode, once you exit proof mode, such as with Qed , all the statements executed within are thereafter considered a single sentence. Back immediately following Qed 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.

Command BackTo natural ¶

This command brings back the system to the state labeled natural , 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 as Back (see above), the BackTo command now handles proof states. For that, it may have to undo some extra commands and end on a state natural ′ ≤ natural if necessary.

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
pretty-printers 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 Section interactive-use).
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 customization-by-environment-variables).
Command Timeout natural sentence¶
Executes sentence. If the operation
has not terminated after natural seconds, then it is interrupted and an error message is
displayed.
Option Default Timeout natural¶
When this option is set, each sentence is treated
as if it was prefixed with Timeout natural, except
for Timeout commands themselves.  If unset, no timeout is
applied.
Command Fail sentence¶
For debugging scripts, sometimes it is desirable to know whether a
command or a tactic fails. If sentence fails, then
Fail sentence succeeds (except for
anomalies or for critical failures such as "stack overflow"), without changing the
proof state.  In interactive mode, the system prints a message
confirming the failure.
Error The command has not failed!¶
If the given command succeeds, then Fail sentence
fails with this error message.
Command Succeed sentence¶
If sentence succeeds, then Succeed sentence succeeds without changing the
proof state.  If sentence fails, then Succeed sentence fails showing the error
message for sentence.
In interactive mode, the system prints the message The command has succeeded and its effects have been reverted. confirming the success.
This command can be useful for writing tests.
Time, Redirect, Timeout, Fail and Succeed are
control_commands. 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 comma-separated 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 to -A.
Option Debug "-? ident+,"¶
This option configures the display of debug messages. Each ident enables debug messages
for that component, while  -ident disables messages for the component.
all activates or deactivates all other components.  backtrace controls printing of
error backtraces.
Test Debug displays the list of components and their enabled/disabled state.
Option Printing Width natural¶
This option sets which left-aligned 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 natural¶
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 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)
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 high-level 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 flags
Printing Implicit, Printing Coercions, Printing Synth,
Printing Projections, and Printing Notations. To reactivate
the high-level printing features, use the command Unset Printing All.
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 use Undelimit Scope and/or Close 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 with Printing All would make
the goal unreadable.
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.
Attribute bypass_check(guard= yes​no?)¶
This boolean attribute is similar to the Guard Checking flag, but on a per-declaration
basis. Disable guard checking locally with bypass_check(guard).
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.
Attribute bypass_check(positivity= yes​no?)¶
This boolean attribute is similar to the Positivity Checking flag, but on a per-declaration basis.
Disable positivity checking locally with bypass_check(positivity).
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 as -type-in-type command line
argument (see Command line options).
Attribute bypass_check(universes= yes​no?)¶
This boolean attribute is similar to the Universe Checking flag, but on a per-declaration basis.
Disable universe checking locally with bypass_check(universes).
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.
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.
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 plug-ins.
Exposing constants to OCaml libraries¶
Command Register qualid1 as qualid2¶
Makes the constant qualid1 accessible to OCaml libraries under
the name qualid2.  The constant can then be dynamically located
in OCaml code by
calling Coqlib.lib_ref "qualid2".  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 qualid2 is kernel,
the constant is exposed to the kernel. For instance, the PrimInt63 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
Primitive Integers
Command Register Inline qualid¶
Gives a hint to the reduction machines (VM and native) that
the body of the constant qualid should be inlined in the generated code.
Command Primitive ident_decl : term? := #ident¶
Makes the primitive type or primitive operator #ident 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 PrimInt63.v and PrimFloat.v use Primitive
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 and
Register with the kernel prefix for other types.  For example,
in PrimInt63.v, #int63_type must be declared before the associated operations.
Error The type ident must be registered before this construction can be typechecked.¶
The type must be defined with Primitive command before this
Primitive command (declaring an operation using the type) will succeed.