| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
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.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This patch also causes the code to finish a bit faster in the NoGlob case
by not preparing a string for dump_string. It also optimizes
Dumpglob.is_ghost by only checking whether the end position is zero.
Note that no ghost locations were part of the glob files of the standard
library before the patch. Note also that the html documentation of the
standard library is bitwise identical before and after the patch.
|
| | |
| |
| |
| |
| | |
We also intepret it at toplevel as a true constr and push the resulting
evarmap in the current state.
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
Now that types can share the same dynamic representation, we do not have
to transtype the topelvel values dynamically and just take advantage of
the standard interpretation function.
|
| | |
| |
| |
| |
| |
| | |
- int and int_or_var
- ident and var
- constr and constr_may_eval
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
When coqtop is a long-lived process (e.g. coqide), the user might be
creating files on the fly. So we have to ask the operating system whether
a file exists beforehand, so that we know whether the content of the
directory cache is outdated.
In batch mode, we can assume that the cache is always up-to-date, so we
don't need to query the operating system before trusting the content of
the cache.
On a script doing "Require Import Reals", this brings down the number of
stat syscalls from 42k to 2k. The number of syscalls could be further
halved if all_subdirs was filling the directory cache.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
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).
|
| | |
| |
| |
| |
| |
| | |
The interesting manifestation of the bug was Unix.select
returning no error but the empty list of descriptors, as if
a timeout did happen.
|
| | | |
|
| | |
| |
| |
| | |
Soon needing a more algebraic view at version numbers...
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| | |
"open Unix" from lib/system.ml.
|
| | | |
|
| | |
| |
| |
| | |
This makes the function sightly more portable.
|
| | | |
|
Pierre-Marie Pédrot
Hugo Herbelin
Maxime Dénès
Guillaume Melquiond
Matej Kosik
Enrico Tassi
Emilio Jesus Gallego Arias