| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
new-tacticals merge. This is essentially a revert of 6fea2f which
broke the sacrosanct backward compatibility of name generation,
thus breaking quite a lot of contribs.
|
|
|
|
supporting metas/evars). Fix of #3169 is by calling pretyping retyper
rather than the non evar-aware kernel type-checker (since argument of
vm_compute is supposed to be already typable).
Support of metas/evars in vm is still to be done...
|
|
|
|
|
|
|
|
|
|
|
|
|
|
parsing is plugged.
|
|
|
|
Serialize.ml spits out its own documentation. Not everything is
statically checked, so it risks to get outdated. Ideas on how
to statically/dynamically check that the doc is in sync are welcome.
|
|
|
