| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | | |
|
| | | |
|
| |/
|
|
| |
Now it is a private field, locations are optional.
|
| |
|
|
| |
It was failing after 1d0eb5d4d6fea.
|
| |
|
|
|
|
|
|
| |
We remove the camlp4 compatibility layer, and try to clean up
most structures. `parsing/compat` is gone.
We added some documentation to the lexer/parser interfaces that are
often obscured by module includes.
|
| |
|
|
| |
This adds at least support for camlp5 6.14 (in addition to 6.17).
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The syntax is: TACTIC EXTEND foo AT LEVEL i
This commit makes it possible to define tacticals like the ssreflect
arrow without having to resort to GEXTEND statements and intepretation
hacks.
Note that it simply makes accessible through the ML interface what Tactic
Notation already supports:
Tactic Notation (at level 1) tactic1(t) "=>" ipats(l) := ...
|
| |/ |
|
| |\ |
|
| | | |
|
| |/ |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
Apparently, in camlp4 (unlike camlp5) :
- Something like "[ kwd = IDENT "foobar" -> .... kwd ... ]"
produces a kwd of type token instead of string (which sounds reasonable ?).
For now, I've replaced kwd by the explicit strings. Not so nice, but works
with both camlp4 and camlp5
- A quotation of the form "let obj = ... in bar; baz" is not
interpreted in the usual OCaml way, but rather as
"(let obj = ... in bar); baz".
Let's use instead "let obj = ... in let () = bar in baz", which works fine.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
|
| | |
|
|
|
We're back to a unique build phase (as before e372b72), but without
relying on the awkward include-deps-failed-lets-retry feature of make.
Since PMP has made grammar/ self-contained, we could now build
grammar.cma in a rather straightforward way, no need for
a specific sub-call to $(MAKE) for that. The dependencies between
files of grammar/ are stated explicitely, since .d files aren't
fully available initially.
Some Makefile simplifications, for instance remove the CAMLP4DEPS
shell horror. Instead, we generalize the use of two different
filename extensions :
- a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp)
- a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo),
except coqide_main.ml4 and its specific rule
Note that we do not generate .ml4.d anymore (thanks to the .mlp vs.
.ml4 dichotomy)
|
Emilio Jesus Gallego Arias
Hugo Herbelin
Gaetan Gilbert
Maxime Dénès
Tej Chajed
Pierre-Marie Pédrot
Pierre Letouzey