| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This patch splits pretty printing representation from IO operations.
- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.
The patch continues work initiated for 8.5 and has the following effects:
- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
`pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
`msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
used instead.
- Feedback provides different backends to handle output, currently,
`stdout`, `emacs` and CoqIDE backends are provided.
- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
gone.
- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
mix.
Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Init/Tauto.v)
|
| |
|
|
|
|
| |
It is indeed confusing, as it has little to do with the proper refine defined
in the New submodule. Legacy code relying on it should call the Logic or
Tacmach modules instead.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |\ \
| | |
| | |
| | | |
trunk
|
| | | | |
|
| | | |
| | |
| | |
| | | |
This reverts commit 23ebfc41fba48ccce9bc878de258d1b0901f7dda.
|
| | | |
| | |
| | |
| | | |
This reverts commit cb6f036b8e097085a849f806aa7c2627b789bd1f.
|
| | | |
| | |
| | |
| | | |
This reverts commit 9df1a3cf26d78df507d0e35c2d9ca987151777be.
|
| | | |
| | |
| | |
| | | |
This reverts commit 857dc0aaae30805725da213b6550dc1ff3a7adb2.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| |\ \ \
| | |/
| |/| |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Bug uncovered by ekcburak@hotmail.com
https://sympa.inria.fr/sympa/arc/coq-club/2016-04/msg00006.html
Now, terms of the the form (Rinv t) are only syntaxified when t evaluates to a non-zero constant.
|
| | | | |
|
| |\ \ \ |
|
| | |/ /
| | |
| | |
| | |
| | |
| | | |
The extraction of [Z] into Ocaml's [Big_int] passed arguments in the
wrong order to [Big.compare_case] for [Pos.compare_cont]. It seems
unlikely this ever worked before.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
printer in the congruence tactic.
Debugging messages were always built even when not in the verbose mode
of congruence.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
It was only used by setoid_ring for the Add Ring command, and was easily
replaced by a dedicated argument. Moreover, it was of no use to tactic
notations.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They
now have to be reachable in the ML code. Note that this has some consequences,
as the previous macro was potentially mixing grammar entries and arguments as
long as their name was the same. Now, each genarg comes with its grammar
instead, so there is no way to abuse the macro.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The ARGUMENT EXTEND macro was discriminating between parsing entries known
statically, i.e. defined in Pcoq and unknown entires. Although simplifying
a bit the life of the plugin writer, it made actual interpretation difficult
to predict and complicated the code of the ARGUMENT EXTEND macro.
After this patch, all parsing entries and generic arguments used in an
ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding
a few more "open Pcoq.X" and "open Constrarg" here and there.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
in cctac which does not support indices properly.
Incidentally, this should fix a failure in RelationAlgebra, where
making prod_applist more robust (e8c47b652) revealed the discriminate
bug in congruence.
|
| | | |
| | |
| | |
| | | |
Fixes compilation of Coq with OCaml 4.03 beta 1.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
It used to allow to represent parts of tactic AST directly in ML code. Most of
the uses were trivial, only calling a constant, except for tauto that had an
important code base written in this style. Removing this reduces the dependency
to CAMLPX and the preeminence of Ltac in ML code.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
This gets rid of brittle code written in ML files through Ltac quotations, and
reduces the dependance of Coq to such a feature. This also fixes the particular
instance of bug #2800, although the underlying issue is still there.
|
Emilio Jesus Gallego Arias
Pierre Letouzey
Pierre-Marie Pédrot
Nickolai Zeldovich
Guillaume Melquiond
Hugo Herbelin
Frédéric Besson
Daniel de Rauglaudre
Maxime Dénès