aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-03-20python3 script does not need to import from the futureRalf Treinen
2020-03-20Add an index for attributes.Théo Zimmermann
2020-03-20Fix the computation of recursive principles with let-bindings.Pierre-Marie Pédrot
2020-03-20Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.Pierre-Marie Pédrot
2020-03-20Merge PR #11814: Document coq_makefile behavior wrt -native-compiler yesEnrico Tassi
2020-03-20Merge PR #11847: Properly thread let-bindings in Funind principle construction.Pierre Courtieu
2020-03-20Merge PR #11778: [ocamformat] Update to 0.13.0Théo Zimmermann
2020-03-20Build and install refman with Dune.Théo Zimmermann
2020-03-20Merge PR #11857: Remove calls to structural equality in MicromegaVincent Laporte
2020-03-19Merge PR #11601: [refman] Move chapters into new structure.Clément Pit-Claudel
2020-03-19[ocamformat] Update to 0.13.0Emilio Jesus Gallego Arias
2020-03-19[obligations] Step towards more structured handling of remaining obligations.Emilio Jesus Gallego Arias
2020-03-19[obligations] Refactor some common code on save pathEmilio Jesus Gallego Arias
2020-03-19[obligations] More progress towards unification of the save pathEmilio Jesus Gallego Arias
2020-03-19[comFixpoint] Cleanup on opens prior to fix unificationEmilio Jesus Gallego Arias
2020-03-19[proof] Remove duplicated poly field in Proof_global.tEmilio Jesus Gallego Arias
2020-03-19[pfedit] Labelize sign parameterEmilio Jesus Gallego Arias
2020-03-19[declare] Remaining bits on the consistency of UState.t namingEmilio Jesus Gallego Arias
2020-03-19[vernac] Make local exception localEmilio Jesus Gallego Arias
2020-03-19[comFixpoing] Refactor hybrid interactive command modalityEmilio Jesus Gallego Arias
2020-03-19[lemmas] Fix comment on public APIEmilio Jesus Gallego Arias
2020-03-19[lemma] Remove double normalization of typesEmilio Jesus Gallego Arias
2020-03-19[declare/lemmas] Make inference hook exception-freeEmilio Jesus Gallego Arias
2020-03-19[ci] Overlays for declare interface refactoring.Emilio Jesus Gallego Arias
2020-03-19[declare] Remove one use of inline_private_constantsEmilio Jesus Gallego Arias
2020-03-19[declare] More uniformity in arguments labels / namesEmilio Jesus Gallego Arias
2020-03-19[declare] Bring more consistency to parameters using labelsEmilio Jesus Gallego Arias
2020-03-19Merge PR #11862: Fix deprecation warning in sphinx and remove workaround for ...Théo Zimmermann
2020-03-19Merge PR #11745: Remove invisible U+FE00 variation selector from CoqIDE bindingsPierre-Marie Pédrot
2020-03-19[refman] Stop using the deprecated math_block node (fixed GH-11856)Clément Pit-Claudel
2020-03-19[refman] Remove workaround for sphinx-doc/sphinx#4983Clément Pit-Claudel
2020-03-19Interpret the Export modifier of Set and Unset as an attribute.Théo Zimmermann
2020-03-19Update fullGrammar, common.edit_mlg and orderedGrammar...Théo Zimmermann
2020-03-19Document all the existing attributes.Théo Zimmermann
2020-03-19Make Cumulative, NonCumulative and Private attributes.Théo Zimmermann
2020-03-19Update fullGrammar and common.edit_mlg following #11839.Théo Zimmermann
2020-03-19Merge PR #11760: firstorder: default tactic is “auto with core”Théo Zimmermann
2020-03-19Adapt to sub-TOC not showing in PDF output.Théo Zimmermann
2020-03-19[refman] Move chapters into new structure.Théo Zimmermann
2020-03-19Remove spurious anomalies in kernel reductionGaëtan Gilbert
2020-03-19Merge PR #11860: [ci] [docker] Update to 4.09.1Gaëtan Gilbert
2020-03-19Fuck off ocamlformat.Pierre-Marie Pédrot
2020-03-19Reduce the scope of a call to pervasive equality in Coq_micromega.Pierre-Marie Pédrot
2020-03-19Merge PR #11795: Print implicit arguments in types of referencesHugo Herbelin
2020-03-19Merge PR #11822: Grants #11692: clear dependent knows about let-inPierre-Marie Pédrot
2020-03-19Use monomorphic comparison functions in Micromega.Vect.Pierre-Marie Pédrot
2020-03-19Dedicate type for monomials in Micromega.Vect.Pierre-Marie Pédrot
2020-03-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-19[stdlib] Remove a few `auto with *`Vincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 05:00:03 +0000