aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-06-27Adding overlay.Hugo Herbelin
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-27Merge PR #7924: Ad hoc fix for #5696, #7903 (ltac subterms and open subterms ...Emilio Jesus Gallego Arias
2018-06-27Slightly less crazy parsing algorithm for CoqProject_file.Pierre-Marie Pédrot
2018-06-27Turn CoqProject_file into a normal OCaml file.Pierre-Marie Pédrot
2018-06-27Fix 'unbound variable' issue on Windows packaging jobs.Théo Zimmermann
2018-06-27Merge PR #7863: Remove Sorts.contentsPierre-Marie Pédrot
2018-06-27Test file for #7723Maxime Dénès
2018-06-27CoqIDE scrolls the proof buffer down to the first goal.Cyprien Mangin
2018-06-27Fix #7723: vm_compute segfaults with universe polymorphismMaxime Dénès
2018-06-27Merge PR #7888: Clarify the message "this hint will only be used by eauto"Pierre-Marie Pédrot
2018-06-26Merge PR #7826: evd: restrict_evar with candidates, can raise NoCandidatesLeftHugo Herbelin
2018-06-26Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).Hugo Herbelin
2018-06-26Merge PR #7906: universes_of_constr don't include universes of monomorphic co...Pierre-Marie Pédrot
2018-06-26Merge PR #7775: Fix handling of universe context for expanded program obligat...Maxime Dénès
2018-06-26Merge PR #7831: Fix for issue #7707: include Ltac2 and Equations in Windows b...Maxime Dénès
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
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 sub...Matthieu Sozeau
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
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
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
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-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
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 kerne...Maxime Dénès
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-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
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-05 11:13:20 +0000