| Age | Commit message (Collapse) | Author |
|---|
|
Ensure correspondence between the term and type to shrink, so that Lets
are preserved when they are used relevantly in either of them. This
avoids e.g. "simpl" in the shrinked hypotheses to reduce shrinking,
while maintaining unsimplified types in the type of the shrinked
obligations (for compatibility).
Simplify Lambda, Prod case of shrinking,
By invariant (we start with a term and its type), the abstraction's
types correspond.
|
|
By default obligations defined by tactics are defined
transparently or opaque according to the Obligations Transparent flag,
except proofs of subset obligations which are treated
as opaque by default. When the user proves the obligation using
Qed or Defined, this information takes precedence, and only
when the obligation cannot be Qed'ed because it contains
references to a recursive function an error is raised
(this prevents the guardness checker error).
Shrinked obligations were not doings this correctly.
Forcing transparency due to fixpoint prototypes
takes precedence over the user preference.
Program: do not force opacity of subset proofs,
maintaining compatibility.
|
|
For compatibility with 8.5.
|
|
Fix bug in Shrink obligations with Program in the process.
Fix implementation of shrink for abstract proofs
- Update doc in term.mli to reflect the fact that let-in's
are part of what is returned by [decompose_lam_assum].
|
|
|
|
|
|
|
|
|
|
|
|
Was PR#223: Allow feedback messages to carry a location.
|
|
The warnings were:
Redundant [RAW_TYPED AS] clause in [ARGUMENT EXTEND cpattern].
Redundant [GLOB_TYPED AS] clause in [ARGUMENT EXTEND cpattern].
Redundant [RAW_TYPED AS] clause in [ARGUMENT EXTEND lcpattern].
Redundant [GLOB_TYPED AS] clause in [ARGUMENT EXTEND lcpattern].
|
|
Was PR#86 Simplify `interp/constrintern.ml:sort_fields`.
|
|
Was PR#225: Patterns-in-binder syntax tests.
|
|
|
|
(Because the function is private to the module, it is documented in
the .ml rather than the .mli)
|
|
The type of the user-defined function "completer" changes to be
simpler and better reflect its purpose: provide values for missing
field assignments. In the future we may want to also pass the name of
the field as parameter (currently only the index is given, and both
uses of the function ignore it), in particular if we want to implement
{ r with x = ...; y = ... }.
|
|
The internal `add_pat` function is replaced by a call to
`CList.extract_first`.
|
|
we already have
val remove_first : ('a -> bool) -> 'a list -> 'a list
(** Remove the first element satisfying a predicate, or raise [Not_found] *)
now we also have the more general
val extract_first : ('a -> bool) -> 'a list -> 'a list * 'a
(** Remove and return the first element satisfying a predicate,
or raise [Not_found] *)
The implementation is tail-recursive. The code I'm hoping to factorize
reimplements extract_first in a tail-recursive way, so it seemed good
to preserve this. On the other hand remove_first is not tail-recursive
itself, and that gives better constant factors in real-life
cases. It's unclear what is the best choice.
|
|
The code was a big "try..with" defining all useful quantities at
once. I tried to lift definitions out of this try..with to define them
as early as possible: the record's information and the first field
name are fetched before processing the other fields.
There were two calls in the try..with body that could raise the
Not_found exception (or at least I don't know the code well enough to
be sure that either of them cannot): `shortest_qualid_of_global` and
`build_patt`. They are now split in two separate try..with blocks,
both raising the same exception (with a shared error message named
`env_error_msg`). Someone familiar with the invariants at play could
probably remove one of the two blocks, streamlining the code even
further.
I'm a bit surprised by the main logic part (the big (if .. else if
.. else if ..) block in the new code), and there is a question in
a comment. I hope to get it answered during code review and remove it
(and maybe simplify the code).
Finally, there was an apparently-stale comment in the code:
(* insertion of Constextern.reference_global *)
of course Constextern.reference_global corresponds to now function
that I could find. After trying to understand the meaning of this
comment, I decided to just remove it.
|
|
|
|
Note that turning
let boolean = not regular in
if boolean && complete then ...;
if boolean && complete then ...;
into
if not regular && complete then ...;
if not regular && complete then ...;
has absolutely no performance cost: negation inside a conditional is
not computed as a boolean, it only flips the branches. The code is
more readable because "boolean" was a terrible variable name.
|
|
|
|
|
|
|
|
Cf CHANGES for details.
|
|
When typing a "with clause fails, type classes are used to possibly
help to insert coercions. If this heuristic fails, do not consider it
anymore to be the best failure since it has made type classes choices
which may be inconsistent with other constraints and on which no
backtracking is possible anymore (see new example in test suite file
4782.v).
This does not mean that using type classes at this point is good. It
may find an instance which help to find a coercion, but which might
still be a choice of instance and coercion which is incompatible with
other constraints.
I tend to think that a convenient way to go to deal with the absence
of backtracking in inserting coercions would be to have special
For the record, here is a some comments of what happens regarding
f9695eb4b and 827663982.
In the presence of an instance (x:=t) given in a "with" clause, with
t:T, and x expected of type T', the situation is the following:
Before f9695eb4b:
- If T and T' are closed and T <= T' is not satisfiable (no coercion
or not convertible), the test for possible insertion of a coercion
is postponed to w_merge, even though there is no way to get more
information since T ant T' are closed. As a result, t may be
ill-typed and the unification may try to unify ill-formed terms,
leading to #4872.
- If T and T' are not closed and contains evars of type a type class,
inference of type classes is tried. If it fails, e.g. because a
wrong type class instance is found, it was postponed to w_merge as
above, and the test for coercion is retried now interleaved with
type classes.
After f9695eb4b and 827663982e:
- If T and T' are closed and T <= T' is not satisfiable (no coercion
or not convertible), the test for possible insertion of a coercion
is an immediate failure. This fixes #4872.
- However, If T and T' are not closed and contains evars of type a
type class, inference of type classes is tried. If it gives closed
terms and fails, this is immediate failure without backtracking on
type classes, resulting in the problem added here to file 4872.v.
The current fix does not consider the result of the use of type
classes while trying to insert a coercion to be the last word on
it. So, it fails with an error which is not the error for conversion
of closed terms (ConversionFailed), therefore in a way expected by
f9695eb4b and 827663982e, and the "with" typing problem is then
postponed again.
|
|
Instead of relaunching the coqtop process and then open the warning window,
we rather fire the warning and wait for the user to press the OK button before
doing anything.
|
|
|
|
I've included some other changes that didn't happen in this PR.
|
|
The ErrorMsg datatype was introduced to allow locations in messages,
however, it was redundant with error and used only in one place.
We remove it in favor of a more uniform treatment of messages with
location. This patch also removes the use of `Loc.ghost` in one place.
Lightly tested.
|
|
The new warnings mechanism may which to forward a location to
IDEs. This also makes sense for other message types.
Next step is to remove redundant MsgError feedback type.
|
|
This is a first step to relay location info in an uniform way, as needed
by warnings and other mechanisms.
The location info remains unused for now, but coqtop printing could take
advantage of it if so wished.
|
|
IMO level indicators are not the proper place to store this information.
|
|
|
|
They were spotted by profiling tactics manipulating huge terms, provided by
Jason Gross.
|
|
Use a much dumber algorithm to recognize the shape of equalities.
|
|
Take advantage that the provided term is always a variable in Equality.is_eq_x.
|
|
|
|
Do not evar-normalize the argument provided by afterHyp.
|
|
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.
|
|
Do not normalize all goals beforehand.
|
|
Do not evar-normalize the term to substitute with. The engine should be
insensitive to this kind of modification.
|
|
We use simple variable substitution instead of full-power term
matching.
|
|
|
|
|
|
|
|
|
|
|
|
Now that the plugins are packed, a plugin forms now a unique
compilation unit, and we only need to install the main cmi file of
this plugin (foo_plugin.cmi).
Btw, better variable names (e.g. OMEGACMO instead of OMEGACMA) and
some other cleanup in Makefile.common (no more INITPLUGINS variable,
for instance).
|
