| Commit message (Collapse) | Author | Age |
|
|
|
|
| |
Fix typeclass resolution which was considering as subgoals
of a tactic application unrelated pre-existing undefined evars.
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
now fails with Error: Already an existential evar of name Main
|
| |
|
|
|
|
|
|
| |
forms in evarconv and unification, as well as fallback to first-order
unification when eta for constructors fail. Update test-suite file
3484 to test for the FO case in evarconv as well.
|
|
|
|
| |
of the record binder for Class C's projections.
|
|
|
|
|
| |
folded primitive projections in applicative stacks in rhs as named, hence
prefering to unfold the lhs in these cases.
|
|
|
|
|
| |
required, i.e. in first-order unification cases where the head of the
other side is a hole or the eta-expanded constant.
|
|
|
|
|
| |
make printing exponentially slower. We would have to expand all projections
at once before detyping to make this linear.
|
| |
|
| |
|
|
|
|
|
|
|
| |
makes"
This makes CatsInZFC explode by expanding constants unnecessarily.
This reverts commit cf36105854c9a42960ee4139c6afdaa75ec8f31a.
|
| |
|
|
|
|
| |
unification.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
new proof engine in e824d4293. Because of the expansion made by "fold"
and possibly by "change", checking the order of hypotheses is
necessary in general in "reduce". Before, it was done by side-effect
on reference "check", now it has to be explicit. To do for
optimization: flag each of the red_expr conversion strategy according
to whether they really need a check.
Also renamed the e_reduce family to e_change to emphasize that some
expansion can occur and that typing has to be rechecked.
This fixes recent failure of CoLoR (and probably Ergo).
|
| |
|
|
|
|
| |
another one.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
This fixes the bug reported by Hugo:
2) Goal True.
3-4) Definition a:=0.
5) Goal True True.
(* jumped back to 3 (on master) instead of 4 (on the outermost proof) *)
|
|
|
|
|
|
|
|
| |
These dependencies between files can be used by UIs to guide compilation
and reloading of files.
FileDependency (Some "/foo.v", "/bar.v") means foo depends on bar.
FileDependency (None, "/bar.v") means the current file depends on bar.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
The problem is that "?[" makes the lexer glue "?" and "[" into
a single token but in ssr "?" (iteration) and "[" (rewrite pattern
delimiter) are often close, but they are parsed by very hard to
refactor grammar entries.
To consider:
- check the adjacency of the two symbols looking at the loc to
parse exactly the same sentences as before this patch
- change syntax completely, e.g. "(_ as id)"
|
| |
|
|
|
|
|
| |
This generalizes the BuildVi flag and lets one choose which
opaque proofs are done and which not.
|
| |
|
|
|
|
|
| |
Now the seff contains it directly, no need to force the future
or to hope that it is a Direct opaque proof.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Before this patch opaque tables were only growing, making them unusable
in interactive mode (leak on Undo).
With this patch the opaque tables are functional and part of the env.
I.e. a constant_body can point to the proof term in 2 ways:
1) directly (before the constant is discharged)
2) indirectly, via an int, that is mapped by the opaque table to
the proof term.
This is now consistent in batch/interactive mode
This is step 0 to make an interactive coqtop able to dump a .vo/.vi
|
| |
|
|
|
|
| |
(interpreting "match goal"'s hypotheses in scope %type).
|
| |
|
|
|
|
|
|
|
| |
for the record binder of classes. This name is no longer generated
in the kernel but part of the declaration. Also cleanup the interface
to recognize primitive records based on an option type instead of a
dynamic check of the length of an array.
|
|
|
|
| |
in cases of unification with existentials requiring it.
|
|
|
|
|
| |
projections and regular records.
Easily fixable backwards incompatibility.
|
|
|
|
| |
and unsatisfiable constraints which were not done in the right environment.
|
|
|
|
|
| |
application case to expand primitive projections at the head of both
applications.
|
|
|
|
| |
expand_projection failing if an innapropriate sigma is given.
|
| |
|
|
|
|
| |
Thanks to Yves for reporting it!
|
| |
|
| |
|
| |
|
|
|
|
| |
Refine.
|