| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
We should really automate the generation of the log of fixes for CHANGES.
|
|
|
|
|
|
|
|
|
|
|
|
Was PR#243: fixing nsatz
|
|
Note that even "Load Verbose" is not supposed to display them.
|
|
The -verbose family of options is only meant to echo sentences as they are
processed. The patch below broke this, while fixing another issue. That
other issue will be fixed in the next commit.
Revert "Fixing "Load" without "Verbose" in coqtop, after vernac_com lost its"
This reverts commit 2a28c677c3c205ff453b7b5903e4c22f4de2649b.
|
|
|
|
|
|
we use a hashtable to reduce the complexity of creating
a duplicate-free list.
|
|
Was PR#199: Unbreak singleton list-like notation (-compat 8.4)
|
|
Was PR#241: Restore option_map in FMapFacts
|
|
|
|
|
|
|
|
the function in_ideal of ideal.ml supposes the list of polynomials
does not contain zero and is duplicate free.
I force this invariant in the call of in_ideal in nsatz.ml4
the function clean_pol returns the reduced list plus a list of
booleans that indicates which polynomials have been deleted
the function expand_pol translates back the certificate of
the reduced to list to the complete list thanks to the list
of booleans.
The fix is quadratic with respect to the input list which should
be ok for reasonable usage of nsatz.
If there is some performance issue we could improve the in_pol
function.
|
|
This way, it's not eaten by a section
|
|
This definition was removed by a4043608f704f026de7eb5167a109ca48e00c221 (This commit adds full universe polymorphism and fast projections to Coq), for reasons I do not know. This means that things like `unfold option_map` work only in 8.5, while `unfold <application of Facts>.option_map` works only in 8.4. This allows `unfold` to work correctly in both 8.4 and 8.5.
|
|
We don't actually need to, unless we want to support the (presumably
uncommon) use-case of someone using [Import VectorNotations] to override
their local notation for things in vector_scope.
Additionally, we now maintain the behavior that [Import VectorNotations]
opens vector_scope.
|
|
In coqtop, one could do for instance:
Require Import Top. (* Where Top contains a Definition b := true *)
Lemma bE : b = true. Proof. reflexivity. Qed.
Definition b := false.
Lemma bad : False. Proof. generalize bE; compute; discriminate. Qed.
That proof could however not be saved because of the circular dependency check.
Safe_typing now checks that we are not requiring (Safe_typing.import) a library
with the same logical name as the current one.
|
|
This fixes bugs #4069 (not 4609 as mentionned in the git log) and #4718.
|
|
Coqc now expects physical names for input files, so fix coq_makefile
accordingly.
|
|
|
|
changing
set (x := val)
into
let x := fresh "x" in
set (x := val)
|
|
|
|
Because refreshing Prop is not semantics-preserving,
the new universe is >= Set, so cannot be minimized to Prop
afterwards.
|
|
This fixes the end of bug #4069, provoked by a use
of unshelve refine which introduces a cast.
|
|
In congruence, refresh universes including the Set/Prop ones so that
congruence works with cumulativity, not restricting itself to the
inferred types of terms that are manipulated but allowing them to be
used at more general types. This fixes bug #4609.
|
|
|
|
We apply this patch to trunk for integration in 8.6 instead.
This reverts commit 715f547816addf3e2e9dc288327fcbcee8c6d47f.
|
|
|
|
Was PR#228: fix coqide double module linking (error on OCaml 4.03)
Fixes #4747: Problem building Coq 8.5pl1 with OCaml 4.03.0: Fatal warnings
triggered by CoqIDE
|
|
|
|
|
|
But there are still bugs with Declare Implicit Tactic, which should
probably rather be reimplemented with ltac:(tac).
Indeed, it does support evars in the type of the term, and
solve_by_implicit_tactic should transfer universe constraints to the
main goal. E.g., the following still fails, at Qed time.
Definition Foo {T}{a : T} : T := a.
Declare Implicit Tactic eassumption.
Goal forall A (x : A), A.
intros.
apply Foo.
Qed.
|
|
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.
|
|
|
|
|
|
|
|
They can apply to the head reference under a notation.
|
|
internalization.
Patch by PMP, test-suite fix by MS.
|
|
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.
|
|
|
