| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |\ |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
This reverts commit 45748e4efae8630cc13b0199dfcc9803341e8cd8.
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
This add LtacProfiling. Much of the code was written by Tobias Tebbi
(@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq
v8.5 and Coq trunk.
|
| |/ |
|
| |\ |
|
| | |
| |
| |
| |
| | |
This breaks compilation via ocamlbuild, and also leads to awkward
commands via make
|
| |/
|
|
| |
Thanks to HH for pointing it out.
|
| |
|
|
|
|
|
| |
This makes the core free from particular protocol choices.
It should help with the ppx serialization project and shrinks clib.cma a
bit.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This eases the task of replacing/improving the serializer, as well as
making it more resistant. See pitfalls below:
Main changes are:
- fold `message` type into `feedback` type
- make messages of type `Richpp.richpp` so we are explicit about the
content being a rich document.
- moved serialization functions for messages and stateid to `Xmlprotocol`
- improved a couple of internal API points (`is_message`).
Tested.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| | |
Coqdep_boot has almost no dependencies, and hence can be compiled
very early during the build, without relying on .ml.d files.
Some code of system.ml is now in a separate file minisys.ml,
which is also included in system.ml for compatibility.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
A non-ASCII char is now converted to _UUxxxx_ with xxxx being its unicode index
in hexa. And any preexisting _UU substring in the ident is converted to _UUU.
The switch from __Uxxxx_ to _UUxxxx_ is cosmetic, it just helps the extraction
(less __ in names). But the other part of the patch (detection of preexisting
_UU substrings) is critical to make ascii_of_ident truly injective and avoid
the following kind of proof of False via native_compute :
Definition α := 1.
Definition __U03b1_ := 2.
Lemma oups : False.
Proof.
assert (α = __U03b1_). { native_compute. reflexivity. }
discriminate.
Qed.
|
| |
|
|
| |
Now the casual Dyn user does not need to be a GADT guru
|
| |\ |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
be used in the generic printer for tactics.
Allows e.g. to print "symmetry in H" correctly after its move to
TACTIC EXTEND.
|
| | |
| |
| |
| |
| |
| |
| | |
This is not perfect yet, in particular the whole precedence system is a real
mess, as there is a real need for tidying up the Pptactic implementation.
Nonetheless, printing toplevel values is only used for debugging purposes, where
an ugly display is better than none at all.
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| | |
hash-consing, so as to avoid having too many kinds of equalities with
same name.
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
We protect Sys.readdir calls againts any nasty exception.
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| | |
This commit also completes 74bd95d10b9f4cccb4bd5b855786c444492b201b
|
| |\| |
|
| | |
| |
| |
| | |
Fixes compilation of Coq with OCaml 4.03 beta 1.
|
| | |
| |
| |
| |
| |
| |
| | |
Printing invalid UTF-8 string startled GTK too much, leading to CoqIDE dying
improperly. We now check that all strings outputed by Coq are proper UTF-8.
This is not perfect, as CoqIDE will sometimes truncate strings which contains
the null character, but at least it should not crash.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
I propose to change the name of the "Util.compose" function to "%".
Reasons:
1. If one wants to express function composition,
then the new name enables us to achieve this goal easier.
2. In "Batteries Included" they had made the same choice.
|
| |\| |
|
| | |
| |
| |
| | |
This fixes micromega in certain environments.
|
| | |
| |
| |
| |
| | |
It is similar to find but raises an assertion failure instead of a Not_found
when the element is not encountered. Using it will give stronger invariants.
|
Cyprien Mangin
Pierre-Marie Pédrot
Jason Gross
Maxime Dénès
Pierre Letouzey
Emilio Jesus Gallego Arias
Enrico Tassi
Tej Chajed
Hugo Herbelin
Matej Kosik