aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-07-12Makefile: no more .ml4.d hence no more rule to clean themPierre Letouzey
2016-07-12".gitignore" updateMatej Kosik
2016-07-12removing ocamldoc-related syntax errorsMatej Kosik
2016-07-12expanding "make help" a little bitMatej Kosik
2016-07-12Removing "READABLE_ML4=" from "Makefile.build"Matej Kosik
2016-07-11Removing "VERBOSE=" from "Makefile.build"Matej Kosik
2016-07-08Fixing the printing of unknown locations by adding a newline.Pierre-Marie Pédrot
2016-07-08Adding a breaking space in warning names.Pierre-Marie Pédrot
2016-07-08Remove spurious warnings about projections when requiring modules.Pierre-Marie Pédrot
2016-07-08Add a few fixes in CHANGES that were forgotten.Maxime Dénès
We should really automate the generation of the log of fixes for CHANGES.
2016-07-08Fix test file for #4858.Maxime Dénès
2016-07-08Fixing #4906 (regression in printing an error message).Hugo Herbelin
2016-07-08Typo in a comment of stdlib.Hugo Herbelin
2016-07-08Add test for pi_eq_proofs.Matthieu Sozeau
2016-07-08Program: Move ProofIrrelevance to Subset.vMatthieu Sozeau
2016-07-08Update csdp.cache.Maxime Dénès
2016-07-08Test file for #4858.Maxime Dénès
2016-07-08Add test file for #4880.Maxime Dénès
2016-07-08Update COPYRIGHT.Maxime Dénès
2016-07-08Merge remote-tracking branch 'github/pr/243' into v8.5Maxime Dénès
Was PR#243: fixing nsatz
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-06improved complexity in nsatzthery
we use a hashtable to reduce the complexity of creating a duplicate-free list.
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-06Bug Fixes : 4851 4858 4880 for nsatzthery
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.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-01 12:55:45 +0000