| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
Rename some functions, remove dead code related to (previously deprecated, now
removed) option Set Boxed Values.
|
| | |
|
| |
|
|
| |
their polymorphic status _and_ locality.
|
| |
|
|
| |
It was wrong, the context was readded needlessly to the local evar_map context.
|
| |
|
|
| |
definitions.
|
| | |
|
| |
|
|
|
| |
The splines=ortho option seems to make dot crash sometimes, so this commit
removes it from the STM debugging output
|
| | |
|
| | |
|
| |
|
|
| |
PIDEtop needs these to implement its new transaction mechanism
|
| |
|
|
|
| |
This lets hooks treat different exceptions in different ways; in
particular, user interrupts can now be safely ignored
|
| | |
|
| |
|
|
| |
Add a flag to disallow minimization to set
|
| | |
|
| |
|
|
|
| |
Retypecheck abstracted infered predicate to register the right
universe constraints.
|
| |
|
|
|
|
| |
We artificially restrict the syntax though, because it is unclear of
what the semantics of several axioms in a row is, in particular about the
resolution of remaining evars.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
- "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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Given the way Lib.extract_hyps is coded if the const_hyps field
of a constant declaration contains a named_context that does not
have the same order of the one in Environment.env, discharging is
broken (as in some section variables are not discharged).
If const_hyps is computed by the kernel, then the order is correct by
construction. If such list is provided by the user, the order is not
granted.
We now systematically sort the list of user provided section hyps.
The code of Proof using is building the named_context in the right
order, but the API was not enforcing/checking it. Now it does.
|
| | |
|
| |
|
|
|
|
| |
According to http://caml.inria.fr/mantis/view.php?id=5325
you can't use the same socket for both writing and reading.
The result is lockups (may be fixed in 4.03).
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
These options can be set to a string value, but also unset.
Internal data is of type string option.
|
| | |
|
| | |
|
| |
|
|
|
| |
Let merge_context_set be lenient when merging the context of side
effects of an entry from solve_by_tac.
|
| | |
|
| |
|
|
|
| |
There is no such thing as the OPTSEP macro in Camlp4 so I had
to expand it by hand.
|
| |
|
|
|
|
|
|
|
| |
This option disallows "declare at first use" semantics for universe
variables (in @{}), forcing the declaration of _all_ universes appearing
in a definition when introducing it with syntax Definition/Inductive
foo@{i j k} .. The bound universes at the end of a definition/inductive
must be exactly those ones, no extras allowed currently.
Test-suite files using the old semantics just disable the option.
|
| |
|
|
|
|
|
| |
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).
|
| |
|
|
| |
universe graph
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
The update process is as follows: run "git shortlog -s -e" and look for
duplicate or missing contributors.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Adding Gérard's history file about V1-V5 versions.
|
| | |
|
| |
|
|
|
|
|
| |
Still, there are small differences, e.g. on
"use_metas_eagerly_in_conv_on_closed_terms", but also maybe in some
amount of use of delta that Matthieu would know better than me if it
matters or not in practice.
|
| | |
|
| |
|
|
|
|
|
| |
context
Let-bound definitions can be opaque but the whole universe context
was not gathered to be discharged at section closing time.
|
| |
|
|
|
|
| |
According to their polymorphic/non-polymorphic status, which
imply that universe variables introduced with it are assumed
to be >= or > Set respectively in the following definitions.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
This relied on universes lower than Prop. A proper test
for the sharing option should be found, -type-in-type is not
enough either.
|
Maxime Dénès
Matthieu Sozeau
Matthieu Sozeau
Alec Faithfull
Enrico Tassi
Pierre-Marie Pédrot
Guillaume Melquiond
Pierre Courtieu
Hugo Herbelin