aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-01-22Remove travisGaëtan Gilbert
The azure OSX job replaces the first travis job, and the second always fails and so is useless.
2019-01-22Transfer maintenance of appveyor infrastructure to the CI teamMaxime Dénès
2019-01-22Merge PR #9225: Fix issue: Windows CI: cygwin install cache is not reused #9212Maxime Dénès
Reviewed-by: maximedenes
2019-01-22[configure] print Sys.os_type since Architecture alone is ambigousEnrico Tassi
2019-01-22[thread] protect threads against sigalrmEnrico Tassi
This makes the implementation of Timeout on unix more reliable since only the main thread will receive the signal for timeout.
2019-01-22Fixing #9329 (registering empty levels in the order they are recomputed).Hugo Herbelin
Was raising an anomaly 'Failure("Grammar.extend")' otherwise.
2019-01-22Merge PR #9308: Remove outdated gitignore coqprojectfile.mlEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-01-22Merge PR #9332: Add OSX job to azureEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego
2019-01-22Make prvect tail recursive (fix #9355)Gaëtan Gilbert
Using a unit test as it's way faster than messing with universes. You can test with universes by ~~~coq Set Universe Polymorphism. Definition x1@{i} := True. Definition x2 := x1 -> x1. Definition x3 := x2 -> x2. Definition x4 := x3 -> x3. Definition x5 := x4 -> x4. Definition x6 := x5 -> x5. Definition x7 := x6 -> x6. Definition x8 := x7 -> x7. Definition x9 := x8 -> x8. Definition x10 := x9 -> x9. Definition x11 := x10 -> x10. Definition x12 := x11 -> x11. Definition x13 := x12 -> x12. Definition x14 := x13 -> x13. Definition x15 := x14 -> x14. Definition x16 := x15 -> x15. Definition x17 := x16 -> x16. Definition x18 := x17 -> x17. Definition x19 := x18 -> x18. About x19. (* 262144 universes *) ~~~ Note on my machine `About x18.` did not overflow even before this commit.
2019-01-22Turn `Refine Instance Mode` off by defaultMaxime Dénès
2019-01-22Make `Add Morphism` not rely on Refine InstanceMaxime Dénès
2019-01-22Remove useless freshness check in new_instanceMaxime Dénès
2019-01-22Distinguish ASTs for Instance and Declare InstanceMaxime Dénès
This makes code paths clearer (we still factorize a lot of the treatment), and we seize the opportunity to forbid anonymous `Declare Instance` which is not a documented construction, and seems to make little sense in practice.
2019-01-22clarify when an ident is added to the clear switchEnrico Tassi
2019-01-22Simplify parsing of instance bindersMaxime Dénès
2019-01-22VernacDeclareClass -> VernacExistingClassMaxime Dénès
2019-01-22VernacDeclareInstances -> VernacExistingInstanceMaxime Dénès
2019-01-22[CS] recognize applied primitive projections as keys (fix #9375)Enrico Tassi
2019-01-22Update CHANGES.mdEnrico
2019-01-22Apply suggestions from code reviewThéo Zimmermann
Co-Authored-By: gares <gares@fettunta.org>
2019-01-21ring and field simplify can take no argumentsthery
2019-01-21[ssr] cleanup of some commentsEnrico Tassi
2019-01-21[ssr] better structure the ipats docEnrico Tassi
2019-01-21Merge PR #9027: Refactor checking of inductive typesMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: mattam82 Ack-by: maximedenes Ack-by: ppedrot
2019-01-21Move plugin tutorial to team ownershipGaëtan Gilbert
2019-01-21Add OSX job to azureGaëtan Gilbert
2019-01-21Refactor typechecking of inductive typesGaëtan Gilbert
We split into smaller functions, use more specific types for universe manipulation, and try to limit how much of the big tuple gets passed to subroutines.
2019-01-21Move inductive typecheck to file independent from positivity check.Gaëtan Gilbert
This is strictly code movement.
2019-01-21Move inductive_error to Type_errorsGaëtan Gilbert
2019-01-21At Qed, if shelved goals remain, emit a warning instead of an errorMaxime Dénès
This error was more or less a debug tool (checking that no tactic breaks the invariant). But some users may want to support other models, see https://github.com/Mtac2/Mtac2/pull/139 for an example discussion.
2019-01-21[EConstr] Expose API to normalize and check if evars are remainingMaxime Dénès
2019-01-21Merge PR #9304: Default disable auto template warning.Maxime Dénès
Reviewed-by: Zimmi48 Reviewed-by: mattam82 Reviewed-by: maximedenes
2019-01-21Merge PR #9340: Add badges linking to a selection of up-to-date Coq packages.Maxime Dénès
Reviewed-by: maximedenes
2019-01-20Discard argument names of section variables on section closeJasper Hugunin
2019-01-20Merge PR #9353: Fix merge-pr.sh when multiple review commentsMaxime Dénès
Reviewed-by: maximedenes
2019-01-19Fix makefile .merlin for unit testsGaëtan Gilbert
2019-01-19[ssr] compile "=> {x..} y" as "=> {x..y} y"Enrico Tassi
This is for consistency with "rewrite {x..} y"
2019-01-19Fix recursive loadpath of ML filesMaxime Dénès
ML files at the root were not taken into account. Coqdep was already doing the right thing.
2019-01-18[ssr] compile "=> {x..}/v" as "/v{x..v}"Enrico Tassi
2019-01-18[ssr] compile "=> {} y" as "=> {y} y"Enrico Tassi
2019-01-18[ssr] clean up implementation of {}/v -> /v{v}Enrico Tassi
2019-01-17Fix merge-pr.sh when multiple review commentsGaëtan Gilbert
It used to output duplicate trailers.
2019-01-17Merge PR #9326: [ci] compile with -quick & validate after vio2voGaëtan Gilbert
Reviewed-by: ejgallego Ack-by: SkySkimmer Ack-by: gares Ack-by: ppedrot
2019-01-17Merge PR #9345: [ci] Update fiat-crypto to the new pipelineGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-01-17Merge PR #9192: Issue #9175, #9190, #9191 (various minor Windows build issues)Maxime Dénès
Reviewed-by: Zimmi48
2019-01-17Merge PR #9048: Fix vernac classification of `Fail Instance`Enrico Tassi
Reviewed-by: gares
2019-01-17Merge PR #9242: merge-pr: add reviewer info to commit messageMaxime Dénès
Reviewed-by: maximedenes Ack-by: ejgallego
2019-01-17Adapt to Coq's new proof mode APIMaxime Dénès
2019-01-16Merge PR #9346: Add .nia.cache to .gitignoreGaëtan Gilbert
2019-01-16Add .nia.cache to .gitignoreJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-25 10:48:42 +0000