| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
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.
|
|
|
|
Note: the choice of the derivative comes from derivable_pt_lim_ps_atan
rather than derivable_pt_atan.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
trunk
|
|
|
|
|
|
and instantiate. Each of these tactics uses it at a different
parsing level, thus actually triggering a parsing error after
merging them. This fix implies some code duplication, which is
a pity. The separation between genargs and parsing entries should
be made one day.
|
|
|
|
|
|
refine tactic, which now uses plain glob_constr's. Now there
is no real need to depend on goal when interpreting genargs.
Possible minor incompatibilities:
1. The interpretation of glob_constr to constr is now done by
Goal.constr_of_raw, which may be slightly dumbier than the dedicated
Tacinterp.interp_open_constr which tries harder. Stdlib and test-suite
do go through, though.
2. I had to change the parsing level of wit_glob in Extraargs
from lconstr to constr. It may break ML notations using glob, but
as they are only used inside Coq code and all well-parenthezised,
it should be OK.
|
|
to old behaviour whenever we were in Program mode.
|
|
|
