| Commit message (Collapse) | Author | Age |
|---|
| |\
| |
| |
| |
| |
| |
| |
| |
| | |
This brings the evaluation model of Ltac closer to those of usual languages, and
further allows the integration of static typing in the long run. More precisely,
toplevel constructed values such as lists and the like do not carry anymore the
type of the underlying data they contain.
This is mostly an API change, as it did not break any contrib outside of mathcomp.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
Although still working, it is now bad practice to use it, and it is not
widely spread anyway.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |/ |
|
| |\ |
|
| | | |
|
| | |\
| | |
| | |
| | | |
into v8.5
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The Haskell extraction code would allow line-wrapping of the Haskell
type definition, which would lead to unparseable Haskell code when the
linebreak occured just before the type name. In particular, with a term
name of 46 characters or more, the following Coq code:
Definition xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx := tt.
Extraction Language Haskell.
Extraction xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx.
would produce:
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx ::
Unit
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx =
Tt
which failed to compile with GHC (according to Haskell's indentation
rules, the "Unit" line must be indented to be treated as a continuation
of the previous line).
This patch always forces the type onto a separate line, and ensures that
it is always indented by 2 spaces (just like the body of each definition).
|
| | | |
| | |
| | |
| | |
| | | |
Note that extracting terms containing primitive projections is still
utterly broken, so don't use them.
|
| | | |
| | |
| | |
| | | |
Patch by Matthieu, Enrico and myself.
|
| |\ \ \
| | | |
| | | |
| | | | |
trunk
|
| | | | |
| | | |
| | | |
| | | | |
A single terminal character can take up to 5 bytes, e.g. "''^A'".
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
preserved, which is a source of incompatibilities w.r.t. released 8.5
but which looks to me to be the only possible canonical behavior.
This is I believe a better behavior than the Regular Subst Tactic
behavior in the released 8.5 and 8.5pl1. There, the order of
hypotheses in which substitutions happened was respected, but their
interleaving with other hypotheses was not respected.
So, I consider this to be a fix to the "Regular Subst Tactic" mode.
Also added a more detailed "specification" of the "Regular" behavior
of "subst" in the reference manual.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
We only retype hypotheses and conclusion when they do depend on the cleared
identifier. This saves a lot of time.
|
| | | | |
| | | |
| | | |
| | | | |
rejected.
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
Disclaimer: I have no idea what I am doing.
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
Also register properly the kind of definition.
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
#4702).
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
When a notation was starting or ending a space, Coq assumed the notation
had no terminal symbol in either places. Coq also considered a notation
containing only spaces to be productive. As stated in the documentation,
extraneous spaces are only meant as printing hints, they are not meant to
have any influence on parsing.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
When encountering a "simpl nomatch" constant, the reduction machinery tries
to unfold it. If the subsequent partial reduction does not produce any
match construct, it keeps going from the reduced term. Unfortunately, the
reduced term has been refolded in the meantime, which means that some of
the previous reduction steps have been canceled, thus causing an infinite
loop. This patch delays the refolding till the very end, so that reduction
always progresses.
Disclaimer: I have no idea what I am doing here. The patch compiles the
standard library and the test suite properly, so hopefully they contain
enough tests to exercise the reduction machinery.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Once again showing the fragility of the parsing engine, commit a7917a32
reversed the relative order of the declaration of parsing rules for tactics
declared through TACTIC EXTEND. There is probably no good order at all, but
for retrocompatibility, this patch enforces the original one.
|
| |\ \ \ \
| | |/ /
| |/| | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Commit 1774a87 increased the file to 1024x1024. This had two adverse
consequences. First, the icon was too large to be used as a window icon
("gdk_window_set_icon_list: icons too large"), so Coqide 8.5 no longer had
an icon at runtime. Second, the file was also used in the About message
box, which was thus exceeding the display size of any reasonably-priced
device. This commit reverts the file to a saner size (still larger than
the original 66x100 picture).
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
As noticed by Cyprien Mangin, projected terms cannot directly be used as
head values. Indeed, they might be applications (e.g. constructors as in
the bug report) whose arguments would thus be missing from the evaluation
stack when doing any iota-reduction step.
The only case where it would make sense is when the evaluation stack is
empty, as an optimization. Indeed, in that case, the arguments are put on
the stack, and then immediately put back inside the term.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Rather than being isolated words, commands and tactics now extend till
dot separators. So bullets can be defined as living only at the top level
of proofs, which should make their detection much more robust.
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
constants up to their canonical name (taken from Daniel's
formalization of Puiseux theorem).
|
| | | | |
| | | |
| | | |
| | | | |
This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15.
|
| | | | |
| | | |
| | | |
| | | | |
This reverts commit f7ea0193c1aac918d8ed2df0d53df38dde5d1152.
|
| | | | |
| | | |
| | | |
| | | | |
This reverts commit c2249c3b4c3387a3c8510e68fc447274d7299695.
|
| | | | |
| | | |
| | | |
| | | | |
This reverts commit 973b6c69f0861c113f7bd5b94604d2497520a334.
|
| | | | |
| | | |
| | | |
| | | | |
This reverts commit 9e9620b99f68622ebaf44c43e9945580f6cc6d98.
|
Pierre-Marie Pédrot
Pierre Letouzey
Hugo Herbelin
Nickolai Zeldovich
Guillaume Melquiond
Maxime Dénès
Matej Kosik