| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
Unset Program Generalized Coercion to avoid coercion of general
applications.
Unset Program Cases to deactivate generation equalities and
disequalities of cases.
|
|
|
|
|
|
|
|
|
|
|
|
When using Record and an explicit sort constraint, the
universe was wrongly made flexible and minimized.
|
|
For better error messages. The API change is
backwards compatible, using a new optional argument.
|
|
When declaring the universes of a lemma explicitely, throw an error if
after minimization the type of a lemma still refers to unbound
universes. This is a fix and an incompatibility, but scripts
will be backwards compatible themselves.
Fix another minor bug in treating universe binders for (Co)Fixpoint.
|
|
Was PR#213: New warnings machinery
|
|
|
|
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
|
|
This allows a work-around for bug #4819,
https://coq.inria.fr/bugs/show_bug.cgi?id=4819.
|
|
This reverts commit 925d258d7d03674c601a1f3832122b3b4b1bc9b0.
I forgot that Jenkins gave me a spurious success when trying to build this PR.
There are a few rough edges to fix, so reverting meanwhile. The Jenkins issue
has been fixed by Matej. Sorry for the noise.
|
|
Otherwise we may backtrack on the resolution in a
by which seems strange.
|
|
Was PR#213: New warnings machinery
|
|
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
|
|
Was PR#207: Add -no-print-dependent-evars
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
