| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
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.
|
| | |
|
| | |
|
| |\
| |
| |
| | |
Was PR#199: Unbreak singleton list-like notation (-compat 8.4)
|
| |\ \
| | |
| | |
| | | |
Was PR#241: Restore option_map in FMapFacts
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | | |
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.
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
It seems like this code was copy-pasted from kernel/inductive.ml. It was
already dubious enough in the kernel. It feels completely wrong in the
checker.
|
| | |
| |
| |
| | |
with recent Coq
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Goal 0=0 -> true=true.
intro H; rewrite H1.
was highlighting H1 but
Goal 0=0 -> true=true.
intro H; rewrite H.
was only highlighting the whole "intro H; rewrite H".
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
With par: the scenario is this one:
coqide --- master ---- proof worker 1 (has no par: steps)
---- proof worker 2 (has a par: step)
---- tac worker 2.1
---- tac worker 2.2
---- tac worker 2.3
Actor 2 installs a remote counter for universe levels, that are
requested to master. Multiple threads dealing with actors 2.x
may need to get values from that counter at the same time.
Long story short, in this complex scenario a mutex was missing
and the control threads for 2.x were accessing the counter (hence
reading/writing to the single socket connecting 2 with master at the
same time, "corrupting" the data flow).
A better solution would be to have a way to generate unique fresh universe
levels locally to a worker.
|
| |\ \ |
|
| |\ \ \ |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Check that the polymorphic status of everything that
is parameterized in nested sections is coherent.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This avoids postponing constraints which will surely produce
an occur-check and allow to backtrack on first-order unifications
producing those constraints directly (e.g. to apply eta).
(fixes HoTT/HoTT with 8.5).
|
| | | | |
| | | |
| | | |
| | | | |
non-recursive notations (#4815).
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Function default_fail was always part of an ise_try. Its associated
error message was anyway thrown away. It is then irrelevant and could
be made simpler.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The tentative fix in f9695eb4b (which I was afraid it might be too
strong, since it was implying failing more often) indeed broke other
things (see #4813).
|
Guillaume Melquiond
Maxime Dénès
Jason Gross
Jason Gross
Matthieu Sozeau
thery
Matthieu Sozeau
Hugo Herbelin
Gabriel Scherer
Pierre-Marie Pédrot
Matej Kosik
Enrico Tassi