| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
Note that this is still broken when loading files containing C-zar scripts.
|
| | |
|
| |
|
|
| |
... in pose proof of large proof terms
|
| | |
|
| |
|
|
|
|
| |
We simply remove the warnings about paths mixing Win32 and Unix
separators, since that situation does not seem problematic (c.f.
discussion on the bug tracker).
|
| |\
| |
| |
| | |
Was PR#335: Fix printing of typeclasses eauto debug wrt intro.
|
| |\ \
| | |
| | |
| | | |
Was PR#336: Remove v62
|
| | | | |
|
| | | |
| | |
| | |
| | | |
Some options are expected to be deprecated
|
| | | |
| | |
| | |
| | |
| | | |
This was not detected by running coq-contribs, so it probably means that
we are not testing with the right version of OCaml.
|
| |\ \ \
| | | |
| | | |
| | | | |
Was PR#340: Fix various shortcomings of the warnings infrastructure.
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
Was PR#341: Better Arguments compatibility.
|
| |/ / / /
| | | |
| | | |
| | | |
| | | | |
With multiple arguments list, repeating the "/" modifier used to be
mandatory. So instead of forbidding it, we issue a deprecation warning.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
- The flags are now interpreted from left to right, without any other
precedence rule. The previous one did not make much sense in interactive
mode.
- Set Warnings and Set Warnings Append are now synonyms, and have the
"append" semantics, which is the most natural one for warnings.
- Warnings on unknown warnings are now printed only once (previously the
would be repeated on further calls to Set Warnings, sections closing,
module requiring...).
- Warning status strings are normalized, so that e.g. "+foo,-foo" is reduced
to "-foo" (if foo exists, "" otherwise).
|
| |/ / /
| | |
| | |
| | | |
This is a better (more generic) fix to #5061 than my e8b9ee76.
|
| | | | |
|
| |\ \ \ |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
(May it fell in the case mentioned in the inner comment of Exninfo.info?)
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Reporting location was not expecting a term passed to an ML tactic to
be interpreted by the ML tactic itself. Made an empirical fix to
report about the as-precise-as-possible location available.
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
Was PR#321: Handling of section variables in hints
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
Was PR#319: More error tagging, try to fix bug 5135
|
| |\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
Was PR#187: Add a META file to support ocamlfind linking.
|
| | | | | | | | |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
This allows building SerAPI and jsCoq using ocamlbuild.
|
| |\ \ \ \ \ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Was PR#337: Fix arguments
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Type annotations in unrelated binders were badly interfering with
detection of recursive binders in notations.
|
| | | | | | | | | |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Instead of circumventing the problem on the caller's side, as was done
in Arguments, we simply avoid failing as there was no real reason for
this anomaly to be triggered. If the list of renamings is shorter than
the one of implicits, we simply interpret the remaining arguments as not
renamed.
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
The main point of this change is to fix #3035: Avoiding trailing
arguments in the Arguments command, and related issues occurring in
HoTT for instance. When the "assert" flag is not specified, we now
accept prefixes of the list of arguments.
The semantics of _ w.r.t. to renaming has changed. Previously, it meant
"restore the original name inferred from the type". Now it means "don't
change the current name".
The syntax of arguments is now restricted. Modifiers like /, ! and
scopes are allowed only in the first arguments list.
We also add *a lot* of missing checks on input values and fix various
bugs.
Note that this code is still way too complex for what it does, due to
the complexity of the implicit arguments, reduction behaviors and renaming
APIs.
|
| | | | | | | | | |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
It used to be Stateid.initial by default. That is indeed a valid
state id but very likely not the very best one (that would be
the tip of the document).
|
| |\ \ \ \ \ \ \ \
| | |_|_|_|/ / /
| |/| | | | | | |
|
| | |\ \ \ \ \ \ \
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
Was PR#338: Remove warning now that info_auto is fixed.
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
Removes a warning dating from 8.5 signaling that info_auto
and info_trivial are broken and advising to use Info 1 auto
instead. Now, these tactics are fixed and thus they can be
used again. They do not do exactly the same thing as
Info 1 auto and may be more useful for the learner.
|
| | | | | | | | | | |
|
| | | | | | | | | | |
|
| | |/ / / / / / /
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
This reverts commit c9c54122d1d9493a965b483939e119d52121d5a6.
This behavior of refine has changed three times in recent years, so
let's take the time to make up our mind and wait for a major release.
Btw, onhyps=None is not a sane way to express that a tactic should be
applied to all hypotheses.
|
| |\ \ \ \ \ \ \ \
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
Was PR#334: Fix bug 5031 : should not be an anomaly
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
not an anomaly
|
| | | | | | | | | | |
|
| | | | | | | | | | |
|
| | | |\ \ \ \ \ \ \
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Was PR#233: Fix a bug in error printing of unif constraints
|
| | | |\ \ \ \ \ \ \ \
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
Was PR#329: Fix #5127 Memory corruption with the VM
|
| |\ \ \ \ \ \ \ \ \ \ \
| | |/ / / / / / / / /
| |/| | | | | | | | | |
|
| | | | | | | | | | | | |
|
| | | | | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
Was PR#301: Update .gitignore with new names for psatz caches.
|
| | | |\ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
Was PR#326: Extend documentation of auto
|
| | | | | | | | | | | | | | |
|
Hugo Herbelin
Matthieu Sozeau
Maxime Dénès
Cyprien Mangin
Jason Gross
Pierre-Marie Pédrot
Emilio Jesus Gallego Arias
Enrico Tassi
Théo Zimmermann
Yves Bertot