| Age | Commit message (Collapse) | Author |
|---|
|
|
|
So adding a test-suite file and closing the bug.
|
|
|
|
They were not parsed correctly with a newline in the middle.
|
|
Add test-suite file to ensure non-regression.
|
|
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.
|
|
|
|
|
|
|
|
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.
|
|
This gets rid of brittle code written in ML files through Ltac quotations, and
reduces the dependance of Coq to such a feature. This also fixes the particular
instance of bug #2800, although the underlying issue is still there.
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
This fixes a TODO in map_constr_expr_with_binders, a bug in
is_constructor, as well as a bug and TODOS in ids_of_cases_indtype.
|
|
evars were created making in turn that evars formerly recognized as
pending were not anymore in the list of pending evars). This also
fixes the reopening of #3848.
See comments on #4484 for details.
|
|
|
|
Also ensure we stay compatible with 8.4: progress could now be made
simply because of beta redexes in the goal.
|
|
|
|
|
|
The side-effects can contain universe declarations needed to typecheck
later proofs, which weren't added to the env used to typecheck them.
|
|
|
|
This commit has deep consequences in term of tactic evaluation,
as it allows to pass any tac_arg to ML and alias tactics rather than
mere generic arguments. This makes the evaluation much more uniform,
and in particular it removes the special evaluation function for notations.
This last point may break some notations out there unluckily.
I had to treat in an ad-hoc way the tactic(...) entry of tactic notations
because it is actually not interpreted as a generic argument but rather
as a proper tactic expression instead.
There is for now no syntax to pass any tactic argument to a given ML or
notation tactic, but this should come soon.
Also fixes bug #3849 en passant.
|
|
The rewrite tactic was causing an evar leak because of the use of the
Evd.remove primitive. This function did not modify the future goals of
the evarmap to remove the considered evar and thus maintained dangling
evars in there, causing the anomaly.
|
|
The previous behavior was to include the interface of such a functor,
possibly leading to the creation of unexpected axioms, see bug report #3746.
In the case of non-functor module with restricted signature, we could
simply refer to the original objects (strengthening), but for a functor,
the inner objects have no existence yet. As said in the new error message,
a simple workaround is hence to first instantiate the functor, then include
the local instance:
Module LocalInstance := Funct(Args).
Include LocalInstance.
By the way, the mod_type_alg field is now filled more systematically,
cf new comments in declarations.mli. This way, we could use it to know
whether a module had been given a restricted signature (via ":"). Earlier,
some mod_type_alg were None in situations not handled by the extraction
(MEapply of module type).
Some code refactoring on the fly.
|
|
|
|
|
|
During an extraction, a few tables are maintained to cache
intermediate results. Due to modules, the kernel_name index
for these caching tables aren't enough. For instance, in
bug #3923, a constant is first transparent (from inside the
module) then opaque (when seen from the signature). The previous
protections were actually obsolete (tests via visible_con), we
now checks that the constant_body is still the same.
|
|
Change was introduced by cedcfc9bc386456f3fdd225f739706e4f7a2902c.
|
|
The unshelve tactical can be used to get the shelved holes. This changes the
proper ordering of holes though, so expect some broken scripts. Also, the
test-suite is not fixed yet.
|
|
|
|
|
|
|
|
|
|
Do not substitute rigid variables during minimization, keeping
their equality constraints instead.
|
|
|
|
|
