| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This tactical is inspired by discussions on the Coq-club list. For now
it is still undocumented, and there is room left for design issues.
|
|
|
|
The clenv_fchain function was needlessly merging universes coming from
two evarmaps even though one was an extension of the other. A flag was
added so that the tactic just retrieves the newer universes.
|
|
We retypecheck the hypotheses introduced by the refine primitive instead of
blindly trusting them when the unsafe flag is set to false.
|
|
is buggy in general.
|
|
its main interest!
|
|
universes are declared correctly in the enclosing proofs evar_map's.
|
|
Side effects are now an opaque data type, called private_constant, you can
only obtain from safe_typing. When add_constant is called on a
definition_entry that contains private constants, they are either
- inlined in the main proof term but not re-checked
- declared globally without re-checking them
As a safety measure, the opaque data type contains a pointer to the
revstruct (an internal field of safe_env that changes every time a new
constant is added), and such pointer is compared with the current value
store in safe_env when the private_constant is inlined. Only when the
comparison is successful the private_constant is not re-checked. Otherwise
else it is. In short, we accept into the kernel private constant only
when they arrive in the very same order and on top of the very same env
they arrived when we fist checked them.
Note: private_constants produced by workers never pass the safety
measure (the revstruct pointer is an Ephemeron). Sending back the
entire revstruct is possible but: 1. we lack a way to quickly compare
two revstructs, 2. it can be large.
|
|
The detection of new hypothesis was bugged.
Now infoH behaves like "Show Intros": it performs tac, grab
information on hypothesis names but let the state unchanged.
FTR: infoH is fundamentally unable to be correct in presence of
tactics that delete hypothesis and reuse there names. Like destruct or
induction. Fortunately destruct and induction now come with a variant
asking that the hypothesis is not deleted. To guess for the right
as-close for [induction H], do [infoH induction !H]. This will not
create the same names as induction would have by itself but at least
there will be the right number of hypothesis.
|
|
|
|
|
|
|
|
Do not normalize the type of a proof according to the final universes
when keep_body_ucst_separate is true, otherwise the type might not be
retypable in the initial context...
|
|
|
|
- "Proof using p*" means: use p and any section var about p.
- Simplify the grammar/parser for proof using <expression>.
- Section variables with a body (let-in) are pulled in automatically
since they are safe to be used (add no extra quantification)
- automatic clear of "unused" section variables made optional:
Set Proof Using Clear Unused.
since clearing section hypotheses does not "always work" (e.g. hint
databases are not really cleaned)
- term_typing: trigger a "suggest proof using" message also for Let
theorems.
|
|
Goal displaying during Debugging ltac is a notice message now. Other
messages are debug messages. This does not change anything in coqide
or coqtop, but allows proofgeneral to dispatch them in the right
buffers (pg had to be fixed too).
|
|
|
|
- When there are side effects which might enrich the initial universes
of a proof, keep the initial and refined universe contexts apart like
for delayed proofs, ensuring universes are declared before they are
used in the right order.
- Fix undefined levels in proof statements so that they can't be lowered
to Set by a subsequent, delayed proof.
|
|
This fixes a bug in proofgeneral. PG will now diplay this message
eagerly. Otherwise since they appear before the goal, they are
considered outdated and not displayed.
|
|
Auto_ind_decl over the internal lemmas. The schemes are built in the
main process and the internal lemmas are actually already also in the
environment.
|
|
|
|
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
|
|
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
|
|
Auto_ind_decl over the internal lemmas. The schemes are built in the
main process and the internal lemmas are actually already also in the
environment.
|
|
|
|
|
|
I used a low-level function, now changed to `msg_notice`.
|
|
Hence we reuse the ones in master.
|
|
|
|
This makes the treatment of universe constraints/normalization more
understandable in the Sync/Async case:
- if one has to keep the constraints of the body and the type of
a lemma separate, then equations coming from the body are kept
(see: 866c41 )
- if they can be merge then the equations (substituted on both the
body and type) can be removed (one of the sides occurs nowhere)
The result is that, semantically, the constraints of a lemma do not
depend on weather it was produced asynchronously (v->vio->vo, or in
a CoqIDE session) or synchronously (v->vo).
Still the internal representation of the constraints changes to
accommodate an optimization (to reduce the size of the constraint set):
- in the synchronous case (some) equations are substituted (in both the
type and body), hence they can be completely dropped from the constraint
set
- in the asynchronous case (some) equations are substituted in the body
only (the type is fixed once and for all before the equations are
discovered/generated), hence these equations are necessary to relate
the type and the (optimized) body and are hence kept in the constraint
set
|
|
Some asynchronous constraints between initial universes and the ones at
the end of a proof were forgotten. Also add a message to print universes
indicating if all the constraints are processed already or not.
|
|
Pretype_errors.PretypeError.
Instad of trying to print the exception, we raise it in the tactic monad.
|
|
Note that this does not prevent using native_compute, but it will force
on-the-fly recompilation of dependencies whenever it is used.
Precompilation is enabled for the standard library, assuming native
compilation was enabled at configuration time.
If native compilation was disabled at configuration time, native_compute
falls back to vm_compute.
Failure to precompile is a hard error, since it is now explicitly required
by the user.
|
|
Some functions from pretyping/typing.ml and their derivatives were potential
source of evarmap leaks, as they dropped their resulting evarmap. This commit
clarifies the situation by renaming them according to a unsafe_* scheme. Their
sound variant is likewise renamed to their old name. The following renamings
were made.
- Typing.type_of -> unsafe_type_of
- Typing.e_type_of -> type_of
- A new e_type_of function that matches the e_ prefix policy
- Tacmach.pf_type_of -> pf_unsafe_type_of
- A new safe pf_type_of function.
All uses of unsafe_* functions should be eventually eliminated.
|
|
Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
|
|
Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593.
As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.
|
|
We just inline the state in the iolist: less closures makes the GC happier.
|
|
|
|
- no more inconsistent Axiom in the Prelude
- STM can now process Admitted proofs asynchronously
- the quick chain can stock "Admitted" jobs in .vio files
- the vio2vo step checks the jobs but does not stock the result
in the opaque tables (they have no slot)
- Admitted emits a warning if the proof is complete
- Admitted uses the (partial) proof term to infer section variables
used (if not given with Proof using), like for Qed
- test-suite: extra line Require TestSuite.admit to each file making
use of admit
- test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to
find TestSuite.admit
|
|
progress.
Also compare goals up to evar instantiation (otherwise no progress would be observed when only unification occurs, unless some [nf_evar] is done). Performance look unchanged so far.
Some code from [Evd] which was used only in [tclPROGRESS] have been moved out (and [progress_evar_map] was now dead, so I killed it).
Fixes bugs (one reported directly on coqdev, and #3412).
|
|
|
|
|
|
|
|
Ultimately setoid rewrite should be written in the monad to fix it properly.
|
|
actually calling the VM at Qed time.
|
|
|
|
|
|
Had to put some hook in the handler of Proofview.NoSuchgoals.
Documentation updated. CHANGE updated.
|
|
Updated doc, but not tests-suite yet.
|
