| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
This reverts commit 5358515f23d1cd47d4914c55dcf049df858b9dc7.
The syntax is deprecated in 8.6, so we now remove it from trunk.
|
| |\ |
|
| | |\
| | |
| | |
| | | |
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.
|
| | |
| |
| |
| |
| |
| |
| | |
Strangely enough, the checker seems to rely on an outdated decompose_app
function which is not the same as the kernel, as the latter is sensitive
to casts. Cast-manipulating functions from the kernel are only used on
upper layers, and thus was moved there.
|
| | |
| |
| |
| |
| | |
We return an option type, as constraints were always dropped if the boolean
was false. They did not make much sense anyway.
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
Before this patch, this module was a member of the library folder, which had
little to do with its actual use. A tiny part relative to global registering
of universe names has been effectively moved to the Global module.
|
| | | |
|
| | | |
|
| |\| |
|
| | |\ |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
(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.
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
generates garbage. So the comment is kept but it is not passed over to ocamldoc.
|
| | | | | | | | |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
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.
|
Pierre-Marie Pédrot
Maxime Dénès
Matej Kosik
Hugo Herbelin
Emilio Jesus Gallego Arias
Enrico Tassi