| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
| |
This is useful for restoring bullets after e.g. loading ssreflect.
Hoping Arnaud is ok in documenting it.
|
| |
|
|
| |
Following a discussion on coq-club on Jan 13, 2016.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
Removed documentation for broken -D -w (but the option are still there).
Fixed documentation of others.
|
| | |
|
| |
|
|
|
|
|
|
| |
enough
In particular, its interface might still change (in interaction with interested
colleagues). So let's not give it too much visibility yet. Instead, I'll turn
it as an opam packages for now.
|
| | |
|
| |
|
|
|
| |
Function is_constructor was not properly fixed. Additionally, this fixes
a problem with the 8.5 interpretation of in-pattern (see Cases.v).
|
| |
|
|
|
| |
This fixes a TODO in map_constr_expr_with_binders, a bug in
is_constructor, as well as a bug and TODOS in ids_of_cases_indtype.
|
| |
|
|
|
|
|
|
| |
evars were created making in turn that evars formerly recognized as
pending were not anymore in the list of pending evars). This also
fixes the reopening of #3848.
See comments on #4484 for details.
|
| | |
|
| |
|
|
| |
constant and arguments _separately_.
|
| | |
|
| |
|
|
|
| |
[rewrite] was calling find_suterm using the wrong unification flags, not
allowing full delta in unification of terms with the right keys as desired.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
On a machine with only 1GB of memory (e.g. in a VM), the compiler might be
abruptly killed by a segfault. We were not getting any feedback in that
case, making it harder to debug.
|
| | |
|
| |
|
|
|
| |
Also ensure we stay compatible with 8.4: progress could now be made
simply because of beta redexes in the goal.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
bug #4477)
The bug was a bit subtle. Function process_cmd_line can be called in three
different ways:
1. tail-recursively to accumulate parsed options in reverse order,
2. directly to parse a file (coqide) or a command line (coq_makefile),
3. recursively to handle a "-f" option.
Once its execution finished, the function reversed its accumulator so
that the parsed options are in correct order. Due to the third case, this
means that the final local order of options was depending on the parity of
the depth of "-f" options. This commit fixes it by changing the function so
that the recursive call gets the actual accumulator rather than its
reversed version.
Warning: this will break all the projects that were inadvertently (or not)
relying on the bug. This might also require a further commit if
coq_makefile itself was relying on the bug.
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
In OCaml 3.x, the toploop of OCaml was accessible from toplevellib.cma. In
OCaml 4.x, it was replaced by compiler-libs. However, linking with
compiler-libs produces a warning (fatal with OCaml 4.03) as soon as we have a
file named errors.ml or lexer.ml...
The only satisfactory solution seems to be to "pack" compiler libs. But it is
not done currently in the OCaml distribution, and implementing it in coqmktop
at this point would be too risky. So for now, I am disabling the warning until
we hear from the OCaml team. In principle, this clash of modules names can
break OCaml's type safety, so we are living dangerously.
|
| |
|
|
|
| |
Linking a module twice is unsafe and warning 31 will be fatal by default in
OCaml 4.03. See PR#5461.
|
| |
|
|
|
|
|
|
| |
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).
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
The side-effects can contain universe declarations needed to typecheck
later proofs, which weren't added to the env used to typecheck them.
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
| |
The rewrite tactic was causing an evar leak because of the use of the
Evd.remove primitive. This function did not modify the future goals of
the evarmap to remove the considered evar and thus maintained dangling
evars in there, causing the anomaly.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The previous behavior was to include the interface of such a functor,
possibly leading to the creation of unexpected axioms, see bug report #3746.
In the case of non-functor module with restricted signature, we could
simply refer to the original objects (strengthening), but for a functor,
the inner objects have no existence yet. As said in the new error message,
a simple workaround is hence to first instantiate the functor, then include
the local instance:
Module LocalInstance := Funct(Args).
Include LocalInstance.
By the way, the mod_type_alg field is now filled more systematically,
cf new comments in declarations.mli. This way, we could use it to know
whether a module had been given a restricted signature (via ":"). Earlier,
some mod_type_alg were None in situations not handled by the extraction
(MEapply of module type).
Some code refactoring on the fly.
|
| | |
|
| |
|
|
|
|
| |
The interesting manifestation of the bug was Unix.select
returning no error but the empty list of descriptors, as if
a timeout did happen.
|
| | |
|
| | |
|
| | |
|
Maxime Dénès
Hugo Herbelin
Matthieu Sozeau
Pierre Courtieu
Pierre Letouzey
Matthieu Sozeau
Enrico Tassi
Guillaume Melquiond
Matej Kosik
Pierre-Marie Pédrot