| Commit message (Collapse) | Author | Age |
... | |
|\| |
|
| | |
|
| | |
|
| | |
|
|\| |
|
| | |
|
| | |
|
|\| |
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
Removed documentation for broken -D -w (but the option are still there).
Fixed documentation of others.
|
| | |
|
| | |
|
|\|
| |
| |
| |
| | |
Conflicts:
lib/cSig.mli
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
|\|
| |
| |
| |
| | |
- Had to add a Sigma.to_evar_map
- Had to rework coqdep_common.ml{,i} and coqdep.ml
|
| |
| |
| |
| |
| |
| |
| | |
Like coqc: detect if the current directory was set by options, if not: add
it with empty logical path.
TODO: check if coq_makefile is still correct wrt to this modification, I
think yes, actually it should end being more correct.
|
| | |
|
|\| |
|
| | |
|
|\| |
|
| |
| |
| |
| | |
(thanks to coq-club, Sep 2015).
|
| | |
|
|\| |
|
| | |
|
| | |
|
|\| |
|
| | |
|
| |
| |
| |
| | |
Useful e.g. with submakefiles.
|
|\| |
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Prior to commit 964d1b70, the dependency files .mllib.d and .mlpack.d
were generated by a call to coqdep using the argument -c (for ocaml
code). While doing some finetuning of the generation of implicit rules,
this commit removed (I think by mistake) this "-c". And without this
-c argument coqdep output nothing on mllib files leading to incorrect
linking of mllibs.
|
|\| |
|
| | |
|
|\| |
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
Characters do not need to be escaped in character ranges. It just had the
effect of matching backslashes four times.
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| | |
"This function is deprecated: the runtime system is now able to print
uncaught exceptions as precisely as Printexc.catch does. Moreover, calling
Printexc.catch makes it harder to track the location of the exception
using the debugger or the stack backtrace facility. So, do not use
Printexc.catch in new code."
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Before this commit, coq-tex was reading the .v file and was guessing how
many lines from the coqtop output it should display. Now, it reads the
coqtop output and it guesses how many lines from the .v file it should
display. That way, coq-tex no longer needs to embed a parser; it relies
on coqtop for parsing.
This is much more robust and makes it possible to properly handle script
such as the following one:
Goal { True }
+ { False }.
{ left. exact I. }
As before, if there is a way for a script to produce something that looks
like a prompt (that is, a line that starts with "foo < "), coq-tex will be
badly confused.
|
|\| |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is only a heuristic and it might cause the tool to become awfully
confused if a line ends with "}" yet this is not the end of a tactic
block. Fixing it would require a full-blown Coq parser inside coq-tex.
Example of crazy output:
Coq < Goal { True }
Coq < 1 subgoal
============================
{True} + {False}
Coq < + { False }.
|
|\| |
|
| |
| |
| |
| |
| |
| | |
The quadratic behaviour of list searching probably appears with small
enough samples. With the advent of usable libraries in Coq, and thus many
possible dependencies, better be safe than sorry.
|