| Age | Commit message (Collapse) | Author |
|---|
|
This commit also completes 74bd95d10b9f4cccb4bd5b855786c444492b201b
|
|
Try first to find a keyed subterm without conversion/betaiota on open
terms (that is the usual strategy of rewrite), if this fails, try with full
conversion, incuding betaiota. This makes the test-suite pass again,
retaining efficiency in the most common cases.
|
|
|
|
|
|
The ARGUMENT EXTEND statement was wrongly using a CompatLoc instead of a Loc,
and this was not detected by typing "thanks" to the Gram.action magic. When
using CAMLP4, this was wreaking havoc at runtime, but not when using CAMLP5,
as the locations where sharing the same representation.
|
|
|
|
primitive projections and prop. ext. or univalence, but at least it prevents
known proofs of false (see discussion on #4588).
|
|
Fixes compilation of Coq with OCaml 4.03 beta 1.
|
|
CQQ -> COQ
|
|
|
|
Printing invalid UTF-8 string startled GTK too much, leading to CoqIDE dying
improperly. We now check that all strings outputed by Coq are proper UTF-8.
This is not perfect, as CoqIDE will sometimes truncate strings which contains
the null character, but at least it should not crash.
|
|
Checking that a term was indeed a relation was made too early, as the
decomposition function recognized relations of the form "f (g .. (h x y))
with f, g unary and only h binary. We postpone this check to the very end.
|
|
|
|
|
|
projections in unification.ml
|
|
unification.
|
|
|
|
reflexivity/symmetry/transitivity only need
RelationClasses to be loaded.
|
|
|
|
|
|
Print and Extraction commands may pierce opacity: if the
task producing the proof term is not finished, we wait for
its completion.
In -quick mode no worker is going to process a task, since tasks
are simply stored to disk (and resumed later in -vio2vo mode).
This commit avoids coqc waits forever for a task in order to
Print/Extract the corresponding term. Bug reported privately
by Alec Faithfull.
|
|
|
|
"Instance name : Type." is like "Lemma name : Type", i.e. it starts
a proof. Unfortunately sometimes it does not, so we say VtUnknown.
Still, if there is an open proof, we classify it as a regular Lemma,
i.e. the opacity depends only on the terminator.
This makes CoqIDE and PIDE based UI way more responsive when processing
files containing Instance that are proved by tactics, since they are now
correctly delegated to workers. Bug reported privately by Alec Faithfull.
|
|
The environment put in the goals was not the right one and could lead to
various leaks.
|
|
The setoid_rewrite tactic was not checking that the relation it was looking for
was indeed a relation, i.e. that its type was an arity.
|
|
The current solution may not be totally ideal though. We generate names for
anonymous evars on the fly at printing time, based on the Evar_kind data they
are wearing. This means in particular that the printed name of an anonymous
evar may change in the future because some unrelate evar has been solved or
introduced.
|
|
It used not to be the case when the proof contains Sideff, since
the code was picking the last known state and not necessarily the
first one. Because of side effects the last known state could be
the one corresponding to the side effect (that was executed to, say,
change the parser). This is also related to bug #4530
|
|
|
|
This fixes micromega in certain environments.
|
|
multiple patterns.
|
|
Instead of relying on a costly set union, we take advantage of the fact
that instances are small compared to the set of universes.
|
|
|
|
|
|
This patch was proposed by JH in bug report #4547.
|
|
The performance enhancement introduced by a895b2c0 for non-polymorphic hints
was actually causing a huge regression in the polymorphic case (and was marked
as such). We fix this by only substituting the metas from the evarmap instead
of the whole evarmap.
|
|
For instance, in
Inductive I : nat -> nat -> Prop := C : forall z, let '(x,y) := z in x + y = 0.
the computation of the number of arguments to I was made wrong in bde12b70.
|
|
|
|
|
|
|
|
|
|
We simply handle the "break" in error messages. Not sure it is the
proper bugfix though, we may want to be able to add breaks in such
recursive notations.
|
|
|
|
variables and definitions in sections is unsupported.
|
|
|
|
Fixpoint/Definition.
|
|
(let x := t in u) a that should be reduced. Maybe a different
decomposition/reduction primitive should be used instead.
|
|
(e.g. with deprecated options such as -byte, etc.) since I guess this
is what we expect.
Was probably lost in 81eb133d64ac81cb.
|
|
|
|
|
|
|
