| 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.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
This maintains compatibility, it is debatable if we should use implicit
type information for lets to allow for coercions to fire.
(Problem found in math-comp).
|
| |\ \ \ |
|
| |/ / / |
|
| | | | |
|
| | | | |
|
| |\ \ \ |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Now scheme will not try to build ill-typed dependent analyses
on recursive records with primitive projections but report
a proper error.
Minor change of the API (adding one error case to recursion_scheme_error).
|
| |/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
When defining a (co)recursive inductive with primitive projections on,
which lacks eta-conversion and hence dependent elimination, build only
the associated non-dependent elimination principles, and warn about
this. Also make the printing of the status of an inductive
w.r.t. projections and eta conversion explicit in Print and About.
|
| | | |\
| | | |
| | | |
| | | | |
Was PR#199: Unbreak singleton list-like notation (-compat 8.4)
|
| | | |\ \
| | | | |
| | | | |
| | | | | |
Was PR#241: Restore option_map in FMapFacts
|
| | | | | |
| | | | |
| | | | |
| | | | | |
We also add a Coq86.v compat file.
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| |/ / / /
| | | |
| | | |
| | | | |
They were allowing algebraic universes to slip in terms.
|
| | | | | |
|
| | | | |
| | | |
| | | | |
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.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This reverts commit b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385, reversing
changes made to da99355b4d6de31aec5a660f7afe100190a8e683.
Hugo asked for more discussion on this topic, and it was not in the roadmap. I
merged it prematurely because I thought there was a consensus. Also, I missed
that it was changing coq_makefile. Sorry about that.
|
| | | |
| | |
| | |
| | |
| | | |
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)
|
| | | | |
|
| |\ \ \
| | | |
| | | |
| | | | |
Was PR#229: Bytecode compilation in a new 'make byte' rule apart from 'make world'
|
| | | |\ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
match.""
We apply this patch to trunk so that it is integrated in 8.6.
This reverts commit 0eb08b70f0c576e58912c1fc3ef74f387ad465be.
|
| |\ \ \ \ \
| | |/ / /
| |/| | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| | | | | |
| | | | |
| | | | |
| | | | | |
not in pl2.
|
| | | | | | |
|
| | | |/ /
| |/| |
| | | |
| | | |
| | | |
| | | | |
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
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This was implemented in anticipation of a part of PR#164 that we decided not to
merge.
|
| | | | | | |
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
Was PR#226: CErrors & CClosure
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
lib/cErrors.ml)
|
Pierre-Marie Pédrot
Matthieu Sozeau
Guillaume Melquiond
Maxime Dénès
Jason Gross
Jason Gross
thery
Matej Kosik
Matthieu Sozeau
Pierre Letouzey