| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Universes are kept in normal form w.r.t. equality but not the <=
relation, so the previous check worked almost always but was actually
too strict! In cases like (max(Set,u) = u) when u is declared >= Set it
was failing to find an equality. Applying the KISS principle:
u = v <-> u <= v /\ v <= u.
Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of
a colon in a typing judgment), this was not the case when an algebraic
universe instantiated an evar that appeared in the term. We force their
universe variable status to change in refresh_universes to avoid this.
Fix ind sort inference: Use syntactic universe equality for inductive
sort inference instead of check_leq (which now correctly takes
constraints into account) and simplify code
|
|
Was PR#339: Documenting type class options, typeclasses eauto
|
|
|
|
Was PR#331: Solve_constraints and Set Use Unification Heuristics
|
|
Was PR#321: Handling of section variables in hints
|
|
|
|
Refine fix for bug #4763, fixing #5149
Tactic [Refine.solve_constraints] and global option
Adds a new multi-goal tactic [Refine.solve_constraints] that forces solving of
unification constraints and evar candidates to be solved. run_tactic now calls
[solve_constraints] at every [.], preserving (mostly) the 8.4/8.5 behavior of tactics.
The option allows to unset the forced solving unification constraints at
each ".", letting the user control the places where the use of
heuristics is done.
Fix test-suite files too.
|
|
|
|
|
|
due to cleared/reverted section variables.
This fixes the get_type_of but requires keeping information
around about the section hyps available in goals during resolution.
It's optimized for the non-section case (should incur no cost there),
and the case where no section variables are cleared.
|
|
When printing evar constraints, we ensure that every variable from the
rel context has a name.
|
|
|
|
|
|
Was PR#263: Fast lookup in named contexts
|
|
goal is under focus and which support returning a relevant output.
|
|
|
|
Essentially, we do not reconstruct the named_context_val when the rel_context
is empty.
|
|
Before computing the whd_evar-form of the arguments of an evar, we first
check that it is indeed defined.
|
|
|
|
|
|
Delimit the scope of the failure to ease potential need for debugging
the debugging printer.
Protect against one of the causes of failure (calling
get_family_sort_of with non-synchronized sigma).
|
|
|
|
We used to recompute all fresh named contexts for evars before this patch in
the push_rel_context_to_named_context function. This was incurring a linear
penalty and a memory explosion due to the reallocation of many arrays. Now, we
rather remember the context between evar creations by sharing it in the pretyping
environment.
This can be considered as a fix for bug #4964 even though we might do better.
|
|
|
|
This saves a quadratic allocation by replacing arrays with maps.
|
|
In addition to sharing, we also delay the computation of the environment in
a by-need fashion.
|
|
|
|
We remove in particular a dubious use of an environment in fresh name
generation. The code was using the wrong environment in a function only
depending on the rel context which was resetted most of the time. This
might change the generated names in extremely rare occurences.
|
|
|
|
|
|
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
|
|
|
For better error messages. The API change is
backwards compatible, using a new optional argument.
|
|
Take advantage that the provided term is always a variable in Equality.is_eq_x.
|
|
We do not allocate a closure in the main loop, and do so only when needed.
|
|
We do not check for presence of a variable in a global definition when we know
that this variable was not present in the section.
|
|
We do not recompute shortest name identifier for global references that were
already traversed. Furthermore, we share the computation of identifiers
between invokations of the name generating function.
This drastically speeds up detyping for huge goals, further mitigating the
shortcomings of the fix for bug #4777.
|
|
|
|
unshelve_goals is used to correctly register dependent
subgoals that have to be solved. Resolution may fail to
do so using hints, so we have to put them back as goals
in that case. The shelf is a good interface for doing that.
unifiable can be used outside proofview to detect dependencies
between goals. This might be better in another module.
|
|
Fix typo in proofview
|
|
|
|
This is the "error resiliency" mode for STM
|
|
|
|
|
|
|
|
|
|
You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals
numbered 1 and 3 to 5.
|
|
|
