| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
Linking the same module twice in OCaml can have problematic unintended
consequences and lead to hard-to-understand bugs, see
http://caml.inria.fr/mantis/view.php?id=4231
http://caml.inria.fr/mantis/view.php?id=5461
OCaml has long warned when double-linking happens
Warning 31: files FOO and BAR both define a module named Baz
In 4.03 this error was turned into a warning by default.
Coqide does double-linking by passing both
xml_{lexer,parser,printer}.cmo and lib/clib.cma that already contains
these compilation units to bin/coqide.byte. To fix compilation of
Coqide under 4.03, the present patch removes the .cmo from the
command-line arguments.
P.S.: I checked that this patch applies cleanly to the current trunk
(b161ad97fdc01ac8816341a089365657cebc6d2b). It should also be possible
to add it as a patch on top of the 8.5 archives (for example those
distributed through OPAM) to make them compile under 4.03.
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
They can apply to the head reference under a notation.
|
|
internalization.
Patch by PMP, test-suite fix by MS.
|
|
|
|
|
|
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.
|
