aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-07-08Typo in a comment of stdlib.Hugo Herbelin
2016-07-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-07Merge remote-tracking branch 'github/bug4653' into v8.6Matthieu Sozeau
2016-07-07Prevent "Load" from displaying all the intermediate subgoals.Guillaume Melquiond
Note that even "Load Verbose" is not supposed to display them.
2016-07-07Do not display goals in -compile-verbose mode (bug #4841).Guillaume Melquiond
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.
2016-07-07Do not use implicit type info for (x := t) bindingsMatthieu Sozeau
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).
2016-07-07Merge remote-tracking branch 'github/bug4873' into v8.6Matthieu Sozeau
2016-07-07Program: fix #4873: transparency option not usedMatthieu Sozeau
2016-07-06Update csdp.cache.Maxime Dénès
2016-07-06Fix typo in configure (noticed by Jason).Maxime Dénès
2016-07-06Merge branch 'primproj' into v8.6Matthieu Sozeau
2016-07-06Fix reopened bug #3317.Matthieu Sozeau
2016-07-06Fixed bug #4622.Matthieu Sozeau
2016-07-06Disallow dependent case on prim records w/o etaMatthieu Sozeau
2016-07-06Renaming to more generic has_dependent_elim testMatthieu Sozeau
2016-07-06Move is_prim... to Inductiveops and correct SchemeMatthieu Sozeau
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).
2016-07-06primproj: warning and avoid error.Matthieu Sozeau
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.
2016-07-06Merge remote-tracking branch 'github/pr/199' into v8.5Maxime Dénès
Was PR#199: Unbreak singleton list-like notation (-compat 8.4)
2016-07-06Merge remote-tracking branch 'github/pr/241' into v8.5Maxime Dénès
Was PR#241: Restore option_map in FMapFacts
2016-07-06Fix #4793: Coq 8.6 should accept -compat 8.6Maxime Dénès
We also add a Coq86.v compat file.
2016-07-06Bump version number in preparation for 8.5pl2 release.Maxime Dénès
2016-07-06Fix test-suite file 3690Matthieu Sozeau
2016-07-06Deduplicate some names in .mailmapJason Gross
2016-07-06Univs: fix internalization of (x := T) and castsMatthieu Sozeau
They were allowing algebraic universes to slip in terms.
2016-07-06Fix indentation of configure printoutJason Gross
2016-07-05Move option_map notation upJason Gross
This way, it's not eaten by a section
2016-07-05Restore option_map in FMapFactsJason Gross
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.
2016-07-05Compat84: Don't mess with stdlib modulesJason Gross
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.
2016-07-05Prevent unsafe overwriting of Required modules by toplevel library.Maxime Dénès
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.
2016-07-05congruence fix: test-suite code and update CHANGESMatthieu Sozeau
This fixes bugs #4069 (not 4609 as mentionned in the git log) and #4718.
2016-07-05Revert "Merge remote-tracking branch 'github/pr/229' into trunk"Maxime Dénès
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.
2016-07-05Pass .v files to coqc in Makefile produced by coq_makefile (bug #4896).Guillaume Melquiond
Coqc now expects physical names for input files, so fix coq_makefile accordingly.
2016-07-05Add mailmap entry.Guillaume Melquiond
2016-07-05Bug fix : variable capture in ltac code of Nsatzthery
changing set (x := val) into let x := fresh "x" in set (x := val)
2016-07-05FIX: "dev/doc/changes.txt"Matej Kosik
2016-07-04Merge remote-tracking branch 'github/pr/229' into trunkMaxime Dénès
Was PR#229: Bytecode compilation in a new 'make byte' rule apart from 'make world'
2016-07-04Merge branch 'congruencefix' into v8.5Matthieu Sozeau
2016-07-04Revert "Revert "Improve the interpretation scope of arguments of an ltac ↵Maxime Dénès
match."" We apply this patch to trunk so that it is integrated in 8.6. This reverts commit 0eb08b70f0c576e58912c1fc3ef74f387ad465be.
2016-07-04Merge branch 'v8.5' into trunkMaxime Dénès
2016-07-04congruence: Restrict refreshing to SetMatthieu Sozeau
Because refreshing Prop is not semantics-preserving, the new universe is >= Set, so cannot be minimized to Prop afterwards.
2016-07-04congruence: remove casts of indexed termsMatthieu Sozeau
This fixes the end of bug #4069, provoked by a use of unshelve refine which introduces a cast.
2016-07-04congruence/univs: properly refresh (fix #4609)Matthieu Sozeau
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.
2016-07-04Update CHANGES, the bugfixes for 4527 and 4726 areMatthieu Sozeau
not in pl2.
2016-07-04Mention more fixes in CHANGES before we release pl2.Maxime Dénès
2016-07-04Revert "Improve the interpretation scope of arguments of an ltac match."Maxime Dénès
We apply this patch to trunk for integration in 8.6 instead. This reverts commit 715f547816addf3e2e9dc288327fcbcee8c6d47f.
2016-07-04test-suite: test checking of libraries checksum.Maxime Dénès
2016-07-04Merge remote-tracking branch 'github/pr/228' into v8.5Maxime Dénès
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
2016-07-03Remove lexing of ordinal notations.Maxime Dénès
This was implemented in anticipation of a part of PR#164 that we decided not to merge.
2016-07-03Mention recent renaming of files in dev/doc/changes.txt.Maxime Dénès
2016-07-03Merge branch 'cerrors-cclosure' into trunkMaxime Dénès
Was PR#226: CErrors & CClosure
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 23:01:27 +0000