| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
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]).
|
|
In commit a92a27 (Fix the compilation of pattern matching wrt to variables), I introduced a serious bug in which, in some case, the infered return predicate of a pattern matching would be lifted wrongly. Because I wrote [false] instead of [true] at one location (which prevented creation of aliases and so created shorter named_context than expected).
|
|
success/instantiate.v was a duplicate of bugs/closed/1041.v
|
|
|
|
It would seem that I forgot to include the actual documentation in 1fb883. As a result, the reference manual didn't compile due to missing dependencies.
|
|
My bad, I forgot to fix the classification before comitting.
|
|
I put it in a new chapter of the Addendum of the manual. Which is meant to be dedicated to plugins with short documentation.
|
|
In the code which indents proof scripts, you cannot assume that a single goal is closed at a time (because of dependent subgoals).
This change had been lost in the rebase over the paral-itp commits in october.
|
|
A small plugin to support program deriving (à la Richard Bird) in Coq.
It's fairly simple:
Require Coq.Derive.Derive.
Derive f From g Upto eq As h.
Produces a goal (actually two, but the first one is automatically shelved):
|- eq g ?42
And closing the proof produces two definitions: f is instantiated with the value of ?42 (it's always transparent). And h is instantiated with the content of the proof (it is transparent or opaque depending on whether the proof was closed with Defined or Qed).
|
|
Commit "The commands that initiate proofs…" was a bit hasty in its treatment of Admitted (in an attempt of making things simple, I actually required the proof to be completed for Admitted to go through…).
|
|
|
|
This commit removes the hook.
|
|
We used to keep a lot of information in the global proof environment, for the end-of-proof commands to use. Now that the end commands are dumb, they are better stored in the proof-termination closure allocated by the starting command.
In this commit, we remove the compute_guard parameter.
|
|
proofs end.
The proof ending commands like Qed and Defined had all the control on what happened to the proof when they are closed. In constrast, proof starting commands were dumb: start a proof, give it a name, that's it.
In such a situation if we want to come up with new reasons to open proofs, we would need new proof-closing commands.
In this commit we decide at proof-starting time how to dispatch the various Qed/Defined, etc… By registering a function in the interactive proof environment. This way, proofs are always closed the same but we can invent new ways to start them.
|
|
synchrone.
The previous heuristic is to check whether the proof ends with Qed or not. This modification allows for commands which start proof but may produce transparent term even when the function ends with Qed.
|
|
I use a telescope to represent to goals, and let proofview.ml generate the appropriate existential variables.
|
|
|
