aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/sphinx/addendum/extraction.rst48
-rw-r--r--doc/sphinx/addendum/program.rst8
-rw-r--r--doc/sphinx/addendum/type-classes.rst53
-rw-r--r--doc/sphinx/practical-tools/coq-commands.rst6
-rw-r--r--doc/sphinx/proof-engine/ltac.rst2
-rw-r--r--doc/sphinx/proof-engine/ssreflect-proof-language.rst42
-rw-r--r--doc/sphinx/proof-engine/tactics.rst61
-rw-r--r--plugins/ltac/tacinterp.ml9
-rw-r--r--proofs/proof_global.ml23
-rw-r--r--tactics/class_tactics.ml10
-rw-r--r--vernac/vernacentries.ml8
11 files changed, 199 insertions, 71 deletions
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index b7d05fd6ef..e93b01f14d 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -164,7 +164,7 @@ The type-preserving optimizations are controlled by the following |Coq| options:
.. cmd:: Extraction Inline {+ @qualid }
In addition to the automatic inline feature, the constants
- mentionned by this command will always be inlined during extraction.
+ mentioned by this command will always be inlined during extraction.
.. cmd:: Extraction NoInline {+ @qualid }
@@ -410,6 +410,52 @@ It is possible to instruct the extraction not to use particular filenames.
For |OCaml|, a typical use of these commands is
``Extraction Blacklist String List``.
+Additional settings
+~~~~~~~~~~~~~~~~~~~
+
+.. opt:: Extraction File Comment @string
+ :name: Extraction File Comment
+
+ Provides a comment that is included at the beginning of the output files.
+
+.. opt:: Extraction Flag @num
+ :name: Extraction Flag
+
+ Controls which optimizations are used during extraction, providing a finer-grained
+ control than :flag:`Extraction Optimize`. The bits of :token:`num` are used as a bit mask.
+ Keeping an option off keeps the extracted ML more similar to the Coq term.
+ Values are:
+
+ +-----+-------+----------------------------------------------------------------+
+ | Bit | Value | Optimization (default is on unless noted otherwise) |
+ +-----+-------+----------------------------------------------------------------+
+ | 0 | 1 | Remove local dummy variables |
+ +-----+-------+----------------------------------------------------------------+
+ | 1 | 2 | Use special treatment for fixpoints |
+ +-----+-------+----------------------------------------------------------------+
+ | 2 | 4 | Simplify case with iota-redux |
+ +-----+-------+----------------------------------------------------------------+
+ | 3 | 8 | Factor case branches as functions |
+ +-----+-------+----------------------------------------------------------------+
+ | 4 | 16 | (not available, default false) |
+ +-----+-------+----------------------------------------------------------------+
+ | 5 | 32 | Simplify case as function of one argument |
+ +-----+-------+----------------------------------------------------------------+
+ | 6 | 64 | Simplify case by swapping case and lambda |
+ +-----+-------+----------------------------------------------------------------+
+ | 7 | 128 | Some case optimization |
+ +-----+-------+----------------------------------------------------------------+
+ | 8 | 256 | Push arguments inside a letin |
+ +-----+-------+----------------------------------------------------------------+
+ | 9 | 512 | Use linear let reduction (default false) |
+ +-----+-------+----------------------------------------------------------------+
+ | 10 | 1024 | Use linear beta reduction (default false) |
+ +-----+-------+----------------------------------------------------------------+
+
+.. flag:: Extraction TypeExpand
+
+ If set, fully expand Coq types in ML. See the Coq source code to learn more.
+
Differences between |Coq| and ML type systems
----------------------------------------------
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 429dcbee69..56f84d0ff0 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -95,6 +95,14 @@ coercions.
(the option is on by default). Coercion of subset types and pairs is still
active in this case.
+.. flag:: Program Mode
+
+ Enables the program mode, in which 1) typechecking allows subset coercions and
+ 2) the elaboration of pattern matching of :cmd:`Program Fixpoint` and
+ :cmd:`Program Definition` act
+ like Program Fixpoint/Definition, generating obligations if there are
+ unresolved holes after typechecking.
+
.. _syntactic_control:
Syntactic control over equalities
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 98dfcb2373..43d302114e 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -461,12 +461,12 @@ type, like:
This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``.
-Options
-~~~~~~~
+Settings
+~~~~~~~~
.. flag:: Typeclasses Dependency Order
- This option (on by default since 8.6) respects the dependency order
+ This flag (on by default since 8.6) respects the dependency order
between subgoals, meaning that subgoals on which other subgoals depend
come first, while the non-dependent subgoals were put before
the dependent ones previously (Coq 8.5 and below). This can result in
@@ -475,7 +475,7 @@ Options
.. flag:: Typeclasses Filtered Unification
- This option, available since Coq 8.6 and off by default, switches the
+ This flag, available since Coq 8.6 and off by default, switches the
hint application procedure to a filter-then-unify strategy. To apply a
hint, we first check that the goal *matches* syntactically the
inferred or specified pattern of the hint, and only then try to
@@ -483,13 +483,13 @@ Options
improve performance by calling unification less often, matching
syntactic patterns being very quick. This also provides more control
on the triggering of instances. For example, forcing a constant to
- explicitely appear in the pattern will make it never apply on a goal
+ explicitly appear in the pattern will make it never apply on a goal
where there is a hole in that place.
.. flag:: Typeclasses Limit Intros
- This option (on by default) controls the ability to apply hints while
+ This flag (on by default) controls the ability to apply hints while
avoiding (functional) eta-expansions in the generated proof term. It
does so by allowing hints that conclude in a product to apply to a
goal with a matching product directly, avoiding an introduction.
@@ -503,16 +503,16 @@ Options
.. flag:: Typeclass Resolution For Conversion
- This option (on by default) controls the use of typeclass resolution
+ This flag (on by default) controls the use of typeclass resolution
when a unification problem cannot be solved during elaboration/type
- inference. With this option on, when a unification fails, typeclass
+ inference. With this flag on, when a unification fails, typeclass
resolution is tried before launching unification once again.
.. flag:: Typeclasses Strict Resolution
- Typeclass declarations introduced when this option is set have a
- stricter resolution behavior (the option is off by default). When
+ Typeclass declarations introduced when this flag is set have a
+ stricter resolution behavior (the flag is off by default). When
looking for unifications of a goal with an instance of this class, we
“freeze” all the existentials appearing in the goals, meaning that
they are considered rigid during unification and cannot be
@@ -528,26 +528,40 @@ Options
.. flag:: Typeclasses Unique Instances
- Typeclass declarations introduced when this option is set have a more
- efficient resolution behavior (the option is off by default). When a
+ Typeclass declarations introduced when this flag is set have a more
+ efficient resolution behavior (the flag is off by default). When a
solution to the typeclass goal of this class is found, we never
backtrack on it, assuming that it is canonical.
+.. flag:: Typeclasses Iterative Deepening
+
+ When this flag is set, the proof search strategy is breadth-first search.
+ Otherwise, the search strategy is depth-first search. The default is off.
+ :cmd:`Typeclasses eauto` is another way to set this flag.
+
+.. opt:: Typeclasses Depth @num
+ :name: Typeclasses Depth
+
+ Sets the maximum proof search depth. The default is unbounded.
+ :cmd:`Typeclasses eauto` is another way to set this option.
+
.. flag:: Typeclasses Debug
Controls whether typeclass resolution steps are shown during search. Setting this flag
- also sets :opt:`Typeclasses Debug Verbosity` to 1.
+ also sets :opt:`Typeclasses Debug Verbosity` to 1. :cmd:`Typeclasses eauto`
+ is another way to set this flag.
.. opt:: Typeclasses Debug Verbosity @num
:name: Typeclasses Debug Verbosity
Determines how much information is shown for typeclass resolution steps during search.
1 is the default level. 2 shows additional information such as tried tactics and shelving
- of goals. Setting this option also sets :flag:`Typeclasses Debug`.
+ of goals. Setting this option to 1 or 2 turns on :flag:`Typeclasses Debug`; setting this
+ option to 0 turns that option off.
.. flag:: Refine Instance Mode
- This option allows to switch the behavior of instance declarations made through
+ This flag allows to switch the behavior of instance declarations made through
the Instance command.
+ When it is on (the default), instances that have unsolved holes in
@@ -560,14 +574,17 @@ Typeclasses eauto `:=`
~~~~~~~~~~~~~~~~~~~~~~
.. cmd:: Typeclasses eauto := {? debug} {? {dfs | bfs}} depth
+ :name: Typeclasses eauto
This command allows more global customization of the typeclass
resolution tactic. The semantics of the options are:
+ ``debug`` In debug mode, the trace of successfully applied tactics is
- printed.
+ printed. This value can also be set with :flag:`Typeclasses Debug`.
+ ``dfs, bfs`` This sets the search strategy to depth-first search (the
- default) or breadth-first search.
+ default) or breadth-first search. This value can also be set with
+ :flag:`Typeclasses Iterative Deepening`.
- + ``depth`` This sets the depth limit of the search.
+ + ``depth`` This sets the depth limit of the search. This value can also be set with
+ :opt:`Typeclasses Depth`.
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index de9e327740..9bc67147f7 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -198,10 +198,10 @@ and ``coqtop``, unless stated otherwise:
:-type-in-type: Collapse the universe hierarchy of |Coq|.
.. warning:: This makes the logic inconsistent.
-:-mangle-names *ident*: Experimental: Do not depend on this option. Replace
+:-mangle-names *ident*: *Experimental.* Do not depend on this option. Replace
Coq's auto-generated name scheme with names of the form *ident0*, *ident1*,
- etc. The command ``Set Mangle Names`` turns the behavior on in a document,
- and ``Set Mangle Names Prefix "ident"`` changes the used prefix. This feature
+ etc. Within Coq, the flag :flag:`Mangle Names` turns this behavior on,
+ and the :opt:`Mangle Names Prefix` option sets the prefix to use. This feature
is intended to be used as a linter for developments that want to be robust to
changes in the auto-generated name scheme. The options are provided to
facilitate tracking down problems.
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 0ea8c7be2d..1071682ead 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1208,7 +1208,7 @@ Interactive debugger
.. flag:: Ltac Debug
- This option governs the step-by-step debugger that comes with the |Ltac| interpreter
+ This option governs the step-by-step debugger that comes with the |Ltac| interpreter.
When the debugger is activated, it stops at every step of the evaluation of
the current |Ltac| expression and prints information on what it is doing.
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 3ca0ffe678..9fbac95f0c 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -157,14 +157,24 @@ compatible with the rest of |Coq|, up to a few discrepancies:
(see :ref:`pattern_conditional_ssr`). To use the
generalized form, turn off the |SSR| Boolean ``if`` notation using the command:
``Close Scope boolean_if_scope``.
-+ The following two options can be unset to disable the incompatible
- rewrite syntax and allow reserved identifiers to appear in scripts.
++ The following flags can be unset to make |SSR| more compatible with
+ parts of Coq:
- .. coqtop:: in
+.. flag:: SsrRewrite
+
+ Controls whether the incompatible rewrite syntax is enabled (the default).
+ Disabling the flag makes the syntax compatible with other parts of Coq.
+
+.. flag:: SsrIdents
- Unset SsrRewrite.
- Unset SsrIdents.
+ Controls whether tactics can refer to |SSR|-generated variables that are
+ in the form _xxx_. Scripts with explicit references to such variables
+ are fragile; they are prone to failure if the proof is later modified or
+ if the details of variable name generation change in future releases of Coq.
+ The default is on, which gives an error message when the user tries to
+ create such identifiers. Disabling the flag generates a warning instead,
+ increasing compatibility with other parts of Coq.
|Gallina| extensions
--------------------
@@ -3063,6 +3073,17 @@ An :token:`r_item` can be:
rewrite -[f y x]/(y + _).
+.. flag:: SsrOldRewriteGoalsOrder
+
+ Controls the order in which generated subgoals (side conditions)
+ are added to the
+ proof context. The flag is off by default, which puts subgoals generated
+ by conditional rules first, followed by the main goal. When it is on,
+ the main goal appears first. If your proofs are organized to complete
+ proving the main goal before side conditions, turning the flag on will save you
+ from having to add :tacn:`last first` tactics that would be needed
+ to keep the main goal as the currently focused goal.
+
Remarks and examples
~~~~~~~~~~~~~~~~~~~~
@@ -5428,6 +5449,17 @@ right hand side double , view hint declaration see :ref:`declaring_new_hints_ssr
prenex implicits declaration see :ref:`parametric_polymorphism_ssr`
+Settings
+~~~~~~~~
+
+.. flag:: Debug Ssreflect
+
+ *Developer only.* Print debug information on reflect.
+
+.. flag:: Debug SsrMatching
+
+ *Developer only.* Print debug information on SSR matching.
+
.. rubric:: Footnotes
.. [#1] Unfortunately, even after a call to the Set Printing All command,
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 150aadc15a..ad80cb62e1 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -264,6 +264,11 @@ Applying theorems
This tactic behaves like :tacn:`simple refine` except it performs type checking
without resolution of typeclasses.
+ .. flag:: Debug Unification
+
+ Enables printing traces of unification steps used during
+ elaboration/typechecking and the :tacn:`refine` tactic.
+
.. tacn:: apply @term
:name: apply
@@ -606,6 +611,10 @@ Applying theorems
when the instantiation of a variable cannot be found
(cf. :tacn:`eapply` and :tacn:`apply`).
+.. flag:: Debug Tactic Unification
+
+ Enables printing traces of unification steps in tactic unification.
+ Tactic unification is used in tactics such as :tacn:`apply` and :tacn:`rewrite`.
.. _managingthelocalcontext:
@@ -2096,9 +2105,9 @@ and an explanation of the underlying technique.
Part of the behavior of the ``inversion`` tactic is to generate
equalities between expressions that appeared in the hypothesis that is
being processed. By default, no equalities are generated if they
- relate two proofs (i.e. equalities between :n:`@terms` whose type is in sort
- :g:`Prop`). This behavior can be turned off by using the option
- :flag`Keep Proof Equalities`.
+ relate two proofs (i.e. equalities between :token:`term`\s whose type is in sort
+ :g:`Prop`). This behavior can be turned off by using the
+ :flag:`Keep Proof Equalities` setting.
.. tacv:: inversion @num
@@ -2534,6 +2543,13 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
unresolved bindings into existential variables, if any, instead of
failing. It has the same variants as :tacn:`rewrite` has.
+ .. flag:: Keyed Unification
+
+ Makes higher-order unification used by :tacn:`rewrite` rely on a set of keys to drive
+ unification. The subterms, considered as rewriting candidates, must start with
+ the same key as the left- or right-hand side of the lemma given to rewrite, and the arguments
+ are then unified up to full reduction.
+
.. tacn:: replace @term with @term’
:name: replace
@@ -4503,3 +4519,42 @@ user-defined tactics.
significant changes in your theories to obtain the same result. As a
drawback of the re-engineering of the code, this tactic has also been
completely revised to get a very compact and readable version.
+
+Delaying solving unification constraints
+----------------------------------------
+
+.. tacn:: solve_constraints
+ :name: solve_constraints
+ :undocumented:
+
+.. flag:: Solve Unification Constraints
+
+ By default, after each tactic application, postponed typechecking unification
+ problems are resolved using heuristics. Unsetting this flag disables this
+ behavior, allowing tactics to leave unification constraints unsolved. Use the
+ :tacn:`solve_constraints` tactic at any point to solve the constraints.
+
+Proof maintenance
+-----------------
+
+*Experimental.* Many tactics, such as :tacn:`intros`, can automatically generate names, such
+as "H0" or "H1" for a new hypothesis introduced from a goal. Subsequent proof steps
+may explicitly refer to these names. However, future versions of Coq may not assign
+names exactly the same way, which could cause the proof to fail because the
+new names don't match the explicit references in the proof.
+
+The following "Mangle Names" settings let users find all the
+places where proofs rely on automatically generated names, which can
+then be named explicitly to avoid any incompatibility. These
+settings cause Coq to generate different names, producing errors for
+references to automatically generated names.
+
+.. flag:: Mangle Names
+
+ When set, generated names use the prefix specified in the following
+ option instead of the default prefix.
+
+.. opt:: Mangle Names Prefix @string
+ :name: Mangle Names Prefix
+
+ Specifies the prefix to use when generating names.
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index c4d8072ba5..cf5eb442be 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2048,13 +2048,4 @@ let () =
optread = (fun () -> get_debug () != Tactic_debug.DebugOff);
optwrite = vernac_debug }
-let () =
- let open Goptions in
- declare_bool_option
- { optdepr = false;
- optname = "Ltac debug";
- optkey = ["Debug";"Ltac"];
- optread = (fun () -> get_debug () != Tactic_debug.DebugOff);
- optwrite = vernac_debug }
-
let () = Hook.set Vernacentries.interp_redexp_hook interp_redexp
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 095aa36f03..67e19df0e7 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -271,14 +271,6 @@ let start_dependent_proof id ?(pl=UState.default_univ_decl) str goals terminator
let get_used_variables () = (cur_pstate ()).section_vars
let get_universe_decl () = (cur_pstate ()).universe_decl
-let proof_using_auto_clear = ref false
-let () = Goptions.(declare_bool_option
- { optdepr = false;
- optname = "Proof using Clear Unused";
- optkey = ["Proof";"Using";"Clear";"Unused"];
- optread = (fun () -> !proof_using_auto_clear);
- optwrite = (fun b -> proof_using_auto_clear := b) })
-
let set_used_variables l =
let open Context.Named.Declaration in
let env = Global.env () in
@@ -287,27 +279,26 @@ let set_used_variables l =
let ctx_set =
List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in
let vars_of = Environ.global_vars_set in
- let aux env entry (ctx, all_safe, to_clear as orig) =
+ let aux env entry (ctx, all_safe as orig) =
match entry with
| LocalAssum (x,_) ->
if Id.Set.mem x all_safe then orig
- else (ctx, all_safe, (CAst.make x)::to_clear)
+ else (ctx, all_safe)
| LocalDef (x,bo, ty) as decl ->
if Id.Set.mem x all_safe then orig else
let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
if Id.Set.subset vars all_safe
- then (decl :: ctx, Id.Set.add x all_safe, to_clear)
- else (ctx, all_safe, (CAst.make x) :: to_clear) in
- let ctx, _, to_clear =
- Environ.fold_named_context aux env ~init:(ctx,ctx_set,[]) in
- let to_clear = if !proof_using_auto_clear then to_clear else [] in
+ then (decl :: ctx, Id.Set.add x all_safe)
+ else (ctx, all_safe) in
+ let ctx, _ =
+ Environ.fold_named_context aux env ~init:(ctx,ctx_set) in
match !pstates with
| [] -> raise NoCurrentProof
| p :: rest ->
if not (Option.is_empty p.section_vars) then
CErrors.user_err Pp.(str "Used section variables can be declared only once");
pstates := { p with section_vars = Some ctx} :: rest;
- ctx, to_clear
+ ctx, []
let get_open_goals () =
let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 719d552def..fd2a163f80 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -121,15 +121,7 @@ let () =
optread = get_typeclasses_debug;
optwrite = set_typeclasses_debug; }
-let () =
- declare_bool_option
- { optdepr = false;
- optname = "debug output for typeclasses proof search";
- optkey = ["Debug";"Typeclasses"];
- optread = get_typeclasses_debug;
- optwrite = set_typeclasses_debug; }
-
-let () =
+let _ =
declare_int_option
{ optdepr = false;
optname = "verbosity of debug output for typeclasses proof search";
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a157e01fc1..629df48c82 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1035,13 +1035,9 @@ let vernac_set_used_variables e =
user_err ~hdr:"vernac_set_used_variables"
(str "Unknown variable: " ++ Id.print id))
l;
- let _, to_clear = Proof_global.set_used_variables l in
- let to_clear = List.map (fun x -> x.CAst.v) to_clear in
+ ignore (Proof_global.set_used_variables l);
Proof_global.with_current_proof begin fun _ p ->
- if List.is_empty to_clear then (p, ())
- else
- let tac = Tactics.clear to_clear in
- fst (Pfedit.solve Goal_select.SelectAll None tac p), ()
+ (p, ())
end
(*****************************)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:25:19 +0000