aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-06-26Merge PR #7775: Fix handling of universe context for expanded program ↵Maxime Dénès
obligations.
2018-06-26Merge PR #7831: Fix for issue #7707: include Ltac2 and Equations in Windows ↵Maxime Dénès
build
2018-06-26Merge PR #7756: Fix #7608: missing num package in INSTALL documentation.Maxime Dénès
2018-06-26Merge PR #7783: Move INSTALL.doc to doc/README.md and improve a few things.Maxime Dénès
2018-06-26Merge PR #7919: Fix equality check on global names from native compute.Maxime Dénès
2018-06-26Add overlay for elpiGaëtan Gilbert
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-26Add overlay for Equations, ElpiGaëtan Gilbert
2018-06-26universes_of_constr don't include universes of monomorphic constantsGaëtan Gilbert
Apparently it was not useful. I don't remember what I was thinking when I added it.
2018-06-26Merge PR #7851: Modernize the introduction of the reference manual.Maxime Dénès
2018-06-25Activate the build of Ltac2 and Equations in the Windows installer.Théo Zimmermann
2018-06-25Reuse CI info to know which version of plugins to build on Windows.Théo Zimmermann
2018-06-25Merge PR #7798: Remove hack skipping comparison of algebraic universes in ↵Matthieu Sozeau
subtyping.
2018-06-25Archive the `gallina` toolVincent Laporte
2018-06-25Clarify the message "this hint will only be used by eauto"Armaël Guéneau
2018-06-25Fix for issue 7707: include Ltac2 and Equations in Windows buildMichael Soegtrop
On the way I also fixed some minor issues with calling MakeCoq_MinGW from cygwin.
2018-06-25Merge PR #7559: Existing Class noop when already a class + warning.Matthieu Sozeau
2018-06-25Fix equality check on global names from native compute.Pierre-Marie Pédrot
Not sure it could have led to a soundness bug, but this is definitely serious enough to deserve a backport. Also made the code robust by listing all the constructors.
2018-06-25Mini-update of version history with recent changes.Hugo Herbelin
2018-06-25Critical bugs: added #3243 and Gonthier's bug in lazy machine.Hugo Herbelin
Both reminded by Enrico.
2018-06-25Merge PR #7620: [ssr] rewrite: turn anomaly into regular errorMaxime Dénès
2018-06-24Merge PR #7895: Revert "Add a note about [ci skip] in CI README."Emilio Jesus Gallego Arias
2018-06-24Merge PR #7805: Towards listing the critical bugs of the history of Coq.Théo Zimmermann
2018-06-24Further cleaning of the side-effect API.Pierre-Marie Pédrot
We remove internal functions and types from the API.
2018-06-24Share the role type between the implementations of side-effects.Pierre-Marie Pédrot
We simply exploit a type isomorphism to remove the use of dedicated algebraic types in the kernel which are actually not necessary.
2018-06-24Merge PR #7772: [native_compute] Delay computations with toplevel matchPierre-Marie Pédrot
2018-06-24Documenting the syntax of mutual keywords.Pierre-Marie Pédrot
2018-06-24Added mention of mutual records to CHANGES.Pierre-Marie Pédrot
2018-06-24Adding various tests for mutual records.Pierre-Marie Pédrot
2018-06-24Handle mutual record at the vernac level.Pierre-Marie Pédrot
Highly spaghetti code, hopefully works.
2018-06-24Handle mutual records in upper layers.Pierre-Marie Pédrot
2018-06-24Merge PR #7784: Remove Tutorials from a few other places following #7466.Maxime Dénès
2018-06-23Merge PR #7614: Simplify the code that handles trust of side-effects in ↵Maxime Dénès
kernel typing.
2018-06-23Merge PR #7236: [ssr] simpler semantics for delayed clearsMaxime Dénès
2018-06-23Merge PR #7827: [engine] safe [add_unification_pb] interfacePierre-Marie Pédrot
2018-06-23Fix for compilation with the camlp5-parser branch.Pierre-Marie Pédrot
2018-06-23Merge PR #7750: Handle mutual records in the kernelMaxime Dénès
2018-06-23Adapt the kernel to generate proper data for mutual records.Pierre-Marie Pédrot
Upper layers are still not able to handle mutual records though.
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
This brings more compatibility with handling of mutual primitive records in the kernel.
2018-06-23Change the proj_ind field from MutInd.t to inductive.Pierre-Marie Pédrot
This is a first step towards the acceptance of mutual record types in the kernel.
2018-06-23Merge PR #7715: Simplify the cooking of primitive projections.Maxime Dénès
2018-06-22Merge PR #7600: Faster and cleaner fconstr-to-constr conversion function.Maxime Dénès
2018-06-22Merge PR #7893: Update dpdgraph branch nameThéo Zimmermann
2018-06-22Merge PR #7776: [ssr] Fix rewrite with universesMaxime Dénès
2018-06-22Fix #7704: get_toplevel_path needs normalised argv.(0)Gaëtan Gilbert
When launched through PATH argv.(0) is just the command name. eg "coqtop -compile foo.v" -> argv.(0) = "coqtop" Using executable_name also follows symlinks but this isn't tested to avoid messing with windows. Running Coq through a symlink is not as important as PATH anyways.
2018-06-22Fix handling of universe context for expanded program obligations.Matthieu Sozeau
The universe context was dropped even though it isn't added to the global universes yet. Keep it so that it is properly defined with the constant the expanded obligation appears in.
2018-06-22Remove hack skipping comparison of algebraic universes in subtyping.Gaëtan Gilbert
When inferring [u <= v+k] I replaced the exception and instead add [u <= v]. This is trivially sound and it doesn't seem possible to have the one without the other (except specially for [Set <= v+k] which was already handled). I don't know an example where this used to fail and now succeeds (the point was to remove an anomaly, but the example ~~~ Module Type SG. Definition DG := Type. End SG. Module MG : SG. Definition DG := Type : Type. Fail End MG. ~~~ now fails with universe inconsistency. Fix #7695 (soundness bug!).
2018-06-22Define and use UGraph.enforce_leq_alg for subtyping inferenceGaëtan Gilbert
Not sure if worth using in other places.
2018-06-22[ssr] document {}/viewEnrico Tassi
2018-06-22[ssr] document rewrite {}fooEnrico Tassi
It was used in some examples, but never fully documented
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-19 15:17:38 +0000