| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
The extraction of [Z] into Ocaml's [Big_int] passed arguments in the
wrong order to [Big.compare_case] for [Pos.compare_cont]. It seems
unlikely this ever worked before.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
printer in the congruence tactic.
Debugging messages were always built even when not in the verbose mode
of congruence.
|
| | |
| |
| |
| |
| |
| | |
Falling back to the global setting if not given.
Useful to make Add Morphism fail correctly when the given proof terms
are incomplete. Adapt test-suite file #2848 accordingly.
|
| | |
| |
| |
| |
| |
| | |
product in setoid_rewrite.
Backport of d670c6b6ce from trunk.
|
| |\ \ |
|
| | | | |
|
| |/ /
| |
| |
| |
| | |
Passing `-compat 8.4` now allows the use of `econstructor (tac)`, as in
8.4.
|
| | |
| |
| |
| |
| | |
I introduced this bug in 4c078b0362542908eb2fe1d63f0d867b339953fd;
Coq.Init.Notations.constructor does not take any arguments.
|
| | |
| |
| |
| | |
We no longer need to redefine `refine` (it now shelves by default). Also clean up `constructor` a bit.
|
| | | |
|
| | |
| |
| |
| | |
regression on apply.
|
| | | |
|
| | |
| |
| |
| |
| | |
Return an evar_map with the right universes, when there are no focused
subgoals or the proof is finished.
|
| | |
| |
| |
| |
| | |
It was not accounting for the universe constraints generated by
applications of the coercion.
|
| | |
| |
| |
| | |
The user-provided sort was ignored for them.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This fix is too restrictive. Still, opening a goal for an evar with a
pending conv_pb is unsafe since the user may prove (instantiate it) in
a way not compatible with the conv_pb.
Assigning an evar, in its lowest level API, should enforce that all
related conv_pbs are satisfied by the instance.
This also poses a UI problem, since there is not way to see these
conv_pbs. One could print a goal and say: look, the proof term you give
must validate this equation...
Given that the good fix is not obvious, we revert!
This reverts commit a0e792236c9666df1069753f8f807c12f713dcfb.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This fixes a class of bugs like
refine foo; tactic.
where tactic fails (by resuming the remaining, unsolvable, problems) while
in 8.4 refine was failing.
It is not clear to us (Maxime and myself) if we should call
consider_remaining_unif_problems instead of check_problems_are_solved.
|
| | |
| |
| |
| |
| | |
hash-consing, so as to avoid having too many kinds of equalities with
same name.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
constant/inductive/constructor kernel_name pairs rather than viewing
them from only the user or canonical part.
Hopefully more uniformity in Constr.hasheq (using systematically == on
subterms).
A semantic change: Cooking now indexing again on full pairs of kernel
names rather than only on the canonical names, so as to preserve user
name.
Also, in pair of kernel names, ensuring the compact representation is
used as soon as both names are the same.
|
| | |
| |
| |
| |
| |
| | |
The interpretation of arguments of tactic notations were normalizing the goal
beforehand, which incurred an important time penalty. We now do this argumentwise
which allows to save time in frequent cases, notably tactic arguments.
|
| | |
| |
| |
| |
| | |
As if we were adding : Type. Consistent with inductives with no
declared arity.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
The regression was introduced by efa1c32a4d178, which replaced
unification by conversion when looking for more occurrences of a
subterm. The conversion function called was not the right one, as it
was not inferring constraints.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Due to a change in pretyping, using cast annotations as typing
constraints, the canonical structure problems given to the unification
could contain non-evar-normalized terms, hence we force
evar normalization where necessary to ensure the same CS solutions
can be found. Here the dependency test is fooled by an erasable
dependency, and the following resolution needs a independent codomain
for pop b to be well-scoped.
|
| | |
| |
| |
| | |
We protect Sys.readdir calls againts any nasty exception.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We force the STM to finish after the initialization request so as to raise
exceptions that may have been generated by the initialization process. Likewise,
we simply die when the initialization request fails in CoqIDE instead of just
printing an error message.
This is the fix for the underlying issue of bug #4591, but it does not solve
the bug yet.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
The SIGINT sent to the master coqtop process was lost in a watchdog thread,
so that the STM resulted in an inconsistent state. This patch catches gracefully
the exception and kills the task as if it were normally cancelled. Note that
it probably won't work on non-POSIX architectures, but it does not really
matter because interrupt was already badly handled anyway.
|
| | | |
|
| | |
| |
| |
| | |
Forcefully equating it to the inferred level is not always desirable or possible.
|
| | |
| |
| |
| |
| |
| |
| | |
When generating the OS X Coq + CoqIDE bundle, hdiutil often produces error
5341. This seems to be a known bug on Apple's side, occurring for some sizes of
dmg files. We try to change the current (problematic) size by adding a file
full of random bits.
|
| | |
| |
| |
| | |
So adding a test-suite file and closing the bug.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
E.g., Inductive foo := mkFoo { bla : foo } allowed to define recursive
records with eta for which conversion is incomplete.
- Eta-conversion only applies to BiFinite inductives
- Finiteness information is now checked by the kernel (the constructor types
must be strictly non recursive for BiFinite declarations).
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Modules inserted into the environment were not hashconsed, leading to an
important redundancy, especially in module signatures that are always fully
expanded.
This patch divides by two the size and memory consumption of module-heavy
files by hashconsing modules before putting them in the environment. Note
that this is not a real hashconsing, in the sense that we only hashcons the
inner terms contained in the modules, that are only mapped over. Compilation
time should globally decrease, even though some files definining a lot of
modules may see their compilation time increase.
Some remaining overhead may persist, as for instance module inclusion is not
hashconsed.
|
| | |
| |
| |
| | |
They were not parsed correctly with a newline in the middle.
|
| | |
| |
| |
| | |
Add test-suite file to ensure non-regression.
|
| | |
| |
| |
| | |
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
|
Matej Kosik
Nickolai Zeldovich
Hugo Herbelin
Daniel de Rauglaudre
Matthieu Sozeau
Maxime Dénès
Jason Gross
Jason Gross
Matthieu Sozeau
Gregory Malecha
Enrico Tassi
Pierre-Marie Pédrot