| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
| |
| |
| |
| | |
constants up to their canonical name (taken from Daniel's
formalization of Puiseux theorem).
|
| | |
| |
| |
| |
| | |
not considering conversion of constants over their canonical name but
on their user name. This is observable when delta is off.
|
| | |
| |
| |
| |
| | |
build a default case if the pattern is irrefutable. It did not matter
in practice because we did not check for unused clauses in this case.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
while eta-expanding a notation) + a more serious variant of it
(alpha-conversion incorrect wrt eta-expansion).
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
This was only when compiling with Camlp4 and it was producing an
assertion failure in asmcomp/emitaux.ml at line 226, reported as
OCaml's bug #6243.
Note: The issue of a problematic compilation with 4.01.0 was raised at
last WG.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
I made a confusion between ltac: in constr and ltac: in tactics, the
one needing parentheses in v8.5 but the latter needing parentheses
only in trunk.
This reverts commit f5dc54519f2a62bab2f7b9059e8c3c8dc53619be.
|
| | |
| |
| |
| | |
so that they are not silently computed when not in debugging mode.
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
Will be displayed on the website, but not part of the package.
|
| | |
| |
| |
| |
| | |
computed when not in debugging mode (especially those printing a
command).
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
location set by lexer). This improves on abb4e7b0c by recovering the
lexer location.
AFAICS, it has an effect on lexer's errors Unterminated_comment and
Unterminated_string. The other errors were not wrongly located,
presumably because the Exc_located location added by camlp5 coincided
with the location given by the lexer.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is a follow-up on Matthieu's 7e7b5684
The Definition command was classified incorrectly when a body was provided.
This fix is a bit ad-hoc. A better one would require more expressiveness in
side effect classification, but I'll do it in trunk only since it could impact
plugins.
Thanks a lot to Enrico for his help!
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
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.
|
Hugo Herbelin
Pierre-Marie Pédrot
Tej Chajed
Maxime Dénès
Matej Kosik
Nickolai Zeldovich
Daniel de Rauglaudre
Matthieu Sozeau
Jason Gross
Jason Gross
Matthieu Sozeau
Gregory Malecha
Enrico Tassi