| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
This covers the case e.g. of "xₚ" (until the table of unicode
characters is upgraded!).
|
| |
|
|
|
| |
`Notation ".a" := nat.' was accepted and used for printing but not
recognized in parsing. Now it does. Other examples in test-suite.
|
| |
|
|
|
|
|
|
|
|
|
| |
The warning was pointless since the notation was accepted and parsed
anyway.
We now treat unrecognized unicode characters like ordinary
undefined tokens (e.g. "#" in a bare Coq).
For instance, "aₚ", or ".ₚ", or "?ₚ" now fail with "Undefined token"
rather than "Unsupported Unicode character".
|
| |
|
|
|
| |
It was not very useful as just parsing won't get you very far due to
lack of notation loading.
|
| |
|
|
|
|
|
|
| |
Given the current style in flags.mli no reason to have a function.
A deeper question is why a global flag is needed, in particular the use
in `interp/constrextern.ml` seems strange, the condition in the lexer
should be looked at and I'm not sure about `printing/`.
|
| |
|
|
|
|
| |
Also renaming vernac_com into interp_vernac and eval_expr into
process_vernac to clarify that it does side-effects (on the contrary
of Stm.interp/Vernacentries.interp).
|
| | |
|
| |
|
|
|
| |
Moving set_formatter_out_channel where it naturally closes the
corresponding opening set_formatter_output_functions.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
This is not fully satisfactory though since we would not like to have
"eval_expr" depending on a parsing/lexing/comments state... but it
does because of eval_expr possibly printing the vernac expression
given to it.
|
| |
|
|
|
|
|
|
|
|
| |
8a8caba3).
- Adding cLexer.current_file to the lexer state, i.e. making it a
component of the type "coq_parsable" of lexer state (it was
forgotten in b8ae2de5 and 8a8caba3).
- Inlining save_translator/restore_translator which have now lost most
of their substance.
|
| |
|
|
|
|
|
| |
It was not used any more by coqdoc since b8194b22 (Dec 2010).
The table is now only part of the lexer function closure
(and only in the camlp5 case).
|
| | |
|
| |\ |
|
| | |
| |
| |
| | |
The output was embedding local paths from my machine.
|
| | |
| |
| |
| | |
I've messed up with parts of the compatibility files I had to commit.
|
| |\ \ |
|
| | | |
| | |
| | |
| | | |
branches (see PR #323).
|
| | | |\ |
|
| |\ \ \ \
| | |_|/
| |/| | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We simply explicit that the type is actually referring to the return type,
not to the type of the argument of the pattern-matching. Note that the
heuristic could be enhanced so as to use the same code in both let-style
and match-style pattern-matching, but I'm leaving this for another time.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
When printing evar constraints, we ensure that every variable from the
rel context has a name.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
"msg_debug (mt())" is not identity, so we return back to how it was
done in 8.4, contracting a repeated pattern-matching into one.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Header was missing in last commit.
One day, it would be nice to unify the display of "debug auto" and
"debug eauto"...
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
There was a catch-all clause in the tclORELSE0 function. We now only
catch noncritical exceptions.
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This is more precise and probably clearer (see e.g. thread
"Understanding auto" on coq-club).
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Revert "Inference of return clause: giving uniformly priority to "small inversion"."
This reverts commit 980b434552d73cb990860f8d659b64686f6dbc87.
|
| | | | | |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \
| | |_|_|_|/
| |/| | | | |
|
| |\ \ \ \ \ \ |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
This happens when recursive notations are used to define recursive
notations.
|
| | | |\ \ \ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Was PR#286: Fix the definition of if_then_else for tactics with multiple
success.
|
| | | | | | | | | |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
git worktrees have a .git file instead of a .git directory.
Using Sys.file_exists is a more general solution which gives true in both cases.
|
| | | | | | | | | |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
But maybe it is that how the "Test" message is elaborated is not
intuitive...
|
| | |/| | | | | | |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
(It should apply also interactively.)
|
| | | | | | | | | |
|
| | |\ \ \ \ \ \ \ |
|
| | | |/ / / / / /
| |/| | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Previously, some splipped through and were caught by unrelated calls to
typeclass resolution.
|
Hugo Herbelin
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Maxime Dénès
Théo Zimmermann
Matthieu Sozeau
Matthieu Sozeau