| Commit message (Collapse) | Author | Age |
| |
|
| |
|
|\ |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| | |
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.
|
|\| |
|
| |
| |
| |
| |
| |
| |
| | |
(e.g. with deprecated options such as -byte, etc.) since I guess this
is what we expect.
Was probably lost in 81eb133d64ac81cb.
|
|\| |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The length of the pattern should now be exactly the number of
assumptions and definitions introduced by the destruction or induction,
including the induction hypotheses in case of an induction.
Like for pattern-matching, the local definitions in the argument of
the constructor can be skipped in which case a name is automatically
created for these.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
We can now use the expressivity of GADT to work around historical kludges
of generic arguments.
|
| |
| |
| |
| |
| |
| | |
No more Obj.magic in Genarg. We leverage the expressivity of GADT
coupled with dynamic tags to get rid of unsafety. For now the API
did not change in order to port the legacy code more easily.
|
| | |
|
| |
| |
| |
| | |
This will allow an easier landing of the rewriting of Genarg.
|
| | |
|
| | |
|
| | |
|
|\|
| |
| |
| |
| | |
Conflicts:
lib/cSig.mli
|
| |
| |
| |
| |
| |
| | |
The Map interface of upcoming OCaml 4.03 includes a new union operator. In
order to make our homemade implementation of Maps compatible with OCaml
versions from 3.12 to 4.03, we define our own signatures for Maps.
|
| |
| |
| |
| |
| |
| |
| |
| | |
CString was linked after Serialize, although the later was using CString.equal.
This had not been noticed so far because OCaml was ignoring functions marked as
external in interfaces (which is the case of CString.equal) when considering
link dependencies. This was changed on the OCaml side as part of the fix of
PR#6956, so linking was now failing in several places.
|
| |
| |
| |
| |
| |
| |
| |
| | |
In the original version, ocamldoc markup wasn't used properly thus
ocamldoc output did not in all places make sense.
This commit makes sure that the documentation of the Predicate module
is as clear as the documentation of the Set module (in the standard library).
|
| |
| |
| |
| |
| | |
Note: they do not even seem to have a debugging purpose, so better remove
them before they bitrot.
|
| | |
|