| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
To make this possible the state id has to reach the kernel.
Hence definition_entry has an extra field, and many files had
to be fixed.
|
| | |
|
| |
|
|
|
|
| |
If a Future.computation is already a value v or an exception and
is chained in a greedy way with a function f, then f v is executed
immediately (or the exception is raised).
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
when internalizing a term.
|
| |
|
|
| |
internalization time.
|
| |
|
|
|
|
| |
used, they are automatically flagged as only parsing. CAVEAT: unused
arguments are not typechecked, because they are dropped before the
interpretation phase.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
configure is now just a minimal wrapper around the new configure.ml.
This configure.ml is runned with the same ocaml used during
compilation, and starts with a #load "unix.cma".
For now, this new configure script is meant to be 99% compatible
with the old one. Known incompatibilities : the --foo option format
(with two --) isn't supported anymore, use -foo options instead.
Let me know if you encounter any other changes.
Internals:
- We use our own "run" command (based on Unix.create_process) to avoid
relying on some specific shell (/bin/sh or cmd.exe).
- We should have far less issues with filename quoting under windows
since we almost never rely on (cygwin) shell anymore. This remains
to be fully tested, though.
- dev/ocamldebug-coq is slightly different now, to ease its generation
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
and nia.
|
| | |
|
| |
|
|
| |
interpreter.
|
| | |
|
| |
|
|
|
|
| |
It triggered nonsensical behaviour of list-using tactic
notation. Hopefully or not, nobody uses such notations out of
the test-suite...
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
Attempt to adapt .el files too.
doc/refman/RefMan-uti.tex has still to be fixed.
|
| |\ |
|
| | |
| |
| |
| | |
test-suite pass.
|
| |/
|
|
|
|
| |
Actually, this was wrong, as evars should not appear until interpretation.
Evarmaps were only passed around uselessly, and often fed with dummy or
irrelevant values.
|
| |
|
|
|
| |
If these messages are still relevent to somebody, feel free to
restore them in -debug or any non-default mode of your choice.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
* vars.mli was mentionning Term instead of Constr, leading to a dep cycle
* Having a file named toplevel/toplevel.ml isn't a good idea when we also
have a toplevel/toplevel.mllib that ought to produce a toplevel.cma.
We rename toplevel.ml into Coqloop.ml
* Extra cleanup of toplevel.mllib :
- Ppextra isn't anywhere around (?!)
- Ppvernac was mentionned twice, and rather belongs to printing.mllib anyway
- Vernacexpr is a .mli and shouldn't appear in an .mllib
* During the link, printing.cma now comes after parsing.cma (Ppvernac uses Egramml)
* A few extra -threads in ocamlbuild files (btw, it's a bit sad to need -thread
for coqchk).
|
| | |
|
| | |
|
| |
|
|
| |
function is sufficient to skip the undefined variables.
|
| |
|
|
| |
Coqide compiled with -thread seems to hang for ever at startup under MacOS
|
| |
|
|
|
|
|
|
|
|
|
|
| |
When using libraries I find it convenient (and future proof) to use fully qualified paths in many places. It would be nice to have a convenient short-hand for this so that you can:
From Xxx Require Yyy Zzz.
instead of having to type:
Require Xxx.Yyy Xxx.Zzz.
Signed-off-by: Pierre Boutillier <pierre.boutillier@ens-lyon.org>
|
| |
|
|
|
|
|
| |
This way, [fun A (P : A -> Prop) (X : sigT P) => proj1_sig X] unifies
with [fun A (P : A -> Prop) (X : sigT P) => projT1 X].
This closes Bug 3043.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The generalizded version is eq_proofs_unicity_one_var. We preserve
backwards compatibility, unless someone used nu_left_inv (which was
defined as a Remark(!), but whose type depended on a number of Lets.)
We could keep going in defining one variable variants, but I was lazy.
I'm also not sure if we should be breaking backward compatiblity to
generalize these theorems, if we should make separate files for the
pointed versions, or if we should just have duplicate theorems in each
file. (I'm also not sure if I should call it _one_var or _pointed or
something else.)
This closes Bug 3019.
|
| | |
|
| |
|
|
| |
We use the win32 specific function only if WIN32 is defined
|
| | |
|
| | |
|
| | |
|
| |
|
| |
I used an exception wrapper to report Tactic failures. It had the consequence of making process_vernac_interp_error to look for the backtrace at the wrong place.
|
| |
|
| |
I doubt [catching_error] is performance critical in any way. But it looked silly to allocate a block to [(inner_trace,e)] when [e] was known in advance (and was already named [e]).
|
Enrico Tassi
Pierre-Marie Pédrot
Maxime Dénès
Pierre Letouzey
Pierre Boutillier
Frédéric Besson
Bruno Barras
Matthieu Sozeau
Gregory Malecha
Jason Gross
Pierre Courtieu
Arnaud Spiwack