| Age | Commit message (Collapse) | Author |
|---|
|
Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g.,
`Opaque foo` doesn't break some automation which tries to unfold `foo`.
We have some timeouts in the strategy success file. We should not run
into issues, because we are not really testing how long these take. We
could just as well use `Timeout 60` or longer, we just want to make sure
the file dies more quickly rather than taking over 10^100 steps.
Note that this tactic does not play well with `abstract`; I have a
potentially controversial change that fixes this issue.
One of the lines in the doc comes from
https://github.com/coq/coq/pull/12129#issuecomment-619771556
Co-Authored-By: Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>
Co-Authored-By: Théo Zimmermann <theo.zimmermann@inria.fr>
Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
This is documented in dev/doc/changes.md.
|
|
We favour unfolding of variables over constants because it is more frequent
for the former to depend on the latter. This has huge consequences on a few
extremely slow lines in mathcomp, up to dividing by 3 single-line invocations
that were taking about 30s on my laptop before the patch.
|
|
This is a partial resurrection of #6423 but only for the kernel.
IMHO, we pay a bit of price for this but it is a good safety
measure.
Only warning "4: fragile pattern matching" and "44: open hides a type"
are disabled.
We would like to enable 44 for sure once we do some alias cleanup.
|
|
|
|
|
|
This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.
The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.
We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.
|
|
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
|
|
|
This commit has no impact, since l2r is always false in practice due to
the definition of default_conv.
|
|
definitions. Instead of failing with an anomaly when trying to do
conversion or computation with the vm's, consider polymorphic constants
as being opaque and keep instances around. This way the code is still
correct but (obviously) incomplete for polymorphic definitions and we
avoid introducing an anomaly. The patch does nothing clever, it only
keeps around instances with constants/inductives and compile constant
bodies only for non-polymorphic definitions.
|
|
|
|
|
|
|
|
transparent status of variables and constants.
|
|
But for vm, the kernel should be functional now
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16961 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16915 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
States.freeze takes ~marshallable:bool, so that (only) when we want to
marshal data to disk/network we can ask the freeze functions of the
summary to force lazy values. The flag is propagated to Lib and Summary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16478 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Most of the time, the table registered via Summary.declare_summary
is just a single reference. A new function Summary.ref now allows
to both declare this ref and register it to summary in one shot.
- Clarifications concerning the role of [init_function].
For statically registered tables that don't need a special initializer,
just do nothing there (see the new Summary.nop function).
Beware: now that Summary exports a function named "ref", any code that
do an "open Summary" will probably fail to compile.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16441 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15998 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.
+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
that the kernel conversion solves the delta/delta critical pair the
same way the tactics did. This allows to improve Qed time when slow
down is due to conversion having (arbitrarily) made the wrong choice.
Propagation is done thanks to a new kind of cast called REVERTcast.
Notes:
- Vm conversion not modified
- size of vo generally grows because of additional casts
- this remains a heuristic... for the record, when a reduction tactic
is applied on the goal t leading to new goal t', this is translated
in the kernel in a conversion t' <= t where, hence, reducing in t'
must be preferred; what the propagation of reduction cast to the
kernel does not do is whether it is preferable to first unfold c or
to first compare u' and u in "c u' = c u"; in particular,
intermediate casts are sometimes useful to solve this kind of issues
(this is the case e.g. in Nijmegen/LinAlg/subspace_dim.v where the
combination "simpl;red" needs the intermediate cast to ensure Qed
answers quickly); henceforth the merge of nested casts in mkCast is
deactivated
- for tactic "change", REVERTcast should be used when conversion is in
the hypotheses, but convert_hyp does not (yet) support this (would
require e.g. that convert_hyp overwrite some given hyp id with a
body-cleared let-binding new_id := Cast(old_id,REVERTCast,t))
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14407 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13005 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This commit concerns about the first half of the useless code
mentionned by Oug for coqtop (without plugins). For the moment,
Oug is used in a mode where any elements mentionned in a .mli
is considered to be precious. This already allows to detect and
remove about 600 lines, and more is still to come.
Among the interesting points, the type Entries.specification_entry
and its constructors SPExxx were never used. Large parts of cases.ml
(and hence subtac_cases.ml) were also useless.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12069 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10961 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
MOVITATION: in a forthcoming commit the application of a substitution to a
constant will return a constr and not a constant. The application of a
substitution to a kernel_name will return a kernel_name. Thus "constant"
should be use as a kernel name for references that can be delta-expanded.
KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code
that implements "Canonical Structure"s). The ADT is violated once in this
ocaml module. My feeling is that the implementation of "Canonical Structure"s
should be rewritten to avoid this situation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5796 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
|
