aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-08-16Split the [check_guarded] typing_flag into [check_guarded] (for (co)fixpoints...SimonBoulier
2019-08-16Merge PR #10457: Make rewrite use the registered elimination schemesPierre-Marie Pédrot
2019-08-14Merge PR #10642: Emit Feedback.AddedAxiom in Declare instead of higher layersPierre-Marie Pédrot
2019-08-10Make rewrite use the registered elimination schemesAndreas Lynge
2019-08-09Overlay for #10642Gaëtan Gilbert
2019-08-09Merge PR #10641: Fix regression of #10637 (-emacs arg should set color to `EM...Emilio Jesus Gallego Arias
2019-08-08Emit Feedback.AddedAxiom in Declare instead of higher layersGaëtan Gilbert
2019-08-08Merge PR #10639: map directory read error to empty directoryEmilio Jesus Gallego Arias
2019-08-08Fix regression of #10637 (-emacs arg sets color to `EMACS)Jim Fehrle
2019-08-08Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations involv...Maxime Dénès
2019-08-08map directory read error to empty directoryspanjel
2019-08-07Merge PR #10604: Simplify Lib section handlingEmilio Jesus Gallego Arias
2019-08-07Merge PR #10525: [funind] Miscellaneous code reorganizations and cleanupPierre-Marie Pédrot
2019-08-06[parsing] unify checks for contiguity of tokens in Ltac2 and G_primEnrico Tassi
2019-08-06Merge PR #10557: Fixing #10286 (coqide hangs on invalid filenames)Pierre-Marie Pédrot
2019-08-06Merge PR #10618: Add missing *.exe files to "make clean"Enrico Tassi
2019-08-05Merge PR #10624: Remove reference to removed option Printing Primitive Projec...Théo Zimmermann
2019-08-05Merge PR #10608: Copy edit the Ltac2 documentationJim Fehrle
2019-08-05Remove reference to removed option Printing Primitive Projection CompatibilityJim Fehrle
2019-08-05Merge PR #10585: [coqdoc] Simplify regex for identifiers in commentsVincent Laporte
2019-08-05Merge PR #10445: Split constructive and classical axioms for real numbersVincent Laporte
2019-08-05ConstructiveCauchyReals: make explicit structural recursionVincent Laporte
2019-08-04Add missing file ide/default_bindings_src.exe to "make clean"Jim Fehrle
2019-08-04Merge PR #10579: Remove underscores from inserted texts.Pierre-Marie Pédrot
2019-08-02[lexer]: improve error message on loct_func misuseEnrico Tassi
2019-08-02Merge PR #10543: Remove unused grammar nonterminals and productionsEnrico Tassi
2019-08-02Copy edit the Ltac2 documentationTej Chajed
2019-08-02Merge PR #10553: Use a more traditional definition for uint63_div21 (fixes #1...Maxime Dénès
2019-07-31Merge PR #9811: [stdlib] Remove deprecated module ZlogarithmEmilio Jesus Gallego Arias
2019-07-31Specialize the section API.Pierre-Marie Pédrot
2019-07-31Remove the universe part from the section variable mechanism.Pierre-Marie Pédrot
2019-07-31Code simplification in Lib section handling.Pierre-Marie Pédrot
2019-07-31[funind] Remove export of `generate_functional_principle` and `make_scheme`Emilio Jesus Gallego Arias
2019-07-31[funind] Port aux function to the new tactic engine.Emilio Jesus Gallego Arias
2019-07-31[funind] Port invfun to the new tactic engine.Emilio Jesus Gallego Arias
2019-07-31[funind] Move duplicated `observe_tac` function to indfun_common.Emilio Jesus Gallego Arias
2019-07-31[funind] Move common `make_eq` to funind_common.Emilio Jesus Gallego Arias
2019-07-31[funind] Move principle generation to its own file.Emilio Jesus Gallego Arias
2019-07-31[funind] Derive_correctness is only used in funind, thus more there.Emilio Jesus Gallego Arias
2019-07-30Merge PR #10594: Fix issue #10593 : Software foundations URL changedEmilio Jesus Gallego Arias
2019-07-30Merge PR #10595: [CI/Azure/macOS] Unshallow the homebrew-core repositoryEmilio Jesus Gallego Arias
2019-07-30Merge PR #10430: [Extraction] Add support for primitive integersMaxime Dénès
2019-07-29Use the precondition of diveucl_21 to avoid massaging the dividend.Guillaume Melquiond
2019-07-29Add a non-overflow precondition to diveucl_21 to align it on standard impleme...thery
2019-07-29Add test from #10551.Guillaume Melquiond
2019-07-29Transpose the C code of uint63_div21 to the OCaml implementations.Guillaume Melquiond
2019-07-29Use a more traditional definition for uint63_div21 (fixes #10551).Guillaume Melquiond
2019-07-29[CI/Azure/macOS] Unshallow the homebrew-core repositoryVincent Laporte
2019-07-29Fix issue #10593 : Software foundations URL changedMichael Soegtrop
2019-07-29Document changes by PR 10324Vincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-11 09:05:01 +0000