aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-05-23Emphasizing the "smart"ness of Array.smartfoldmap{,2} in their documentation.Hugo Herbelin
2018-05-23CArray: adding combinators.Hugo Herbelin
2018-05-23Merge PR #7414: Add .byte targets for every bestocaml targetEnrico Tassi
2018-05-23Merge PR #7567: Clean-up dead file in test-suite.Enrico Tassi
2018-05-22Merge PR #7565: Document the new nested-proof error message.Emilio Jesus Gallego Arias
2018-05-22Merge PR #7577: Fixing debugger after #6859 (loading dynlink.cma before lib.c...Emilio Jesus Gallego Arias
2018-05-22Fixing debugger after #6859 (loading dynlink.cma before lib.cma).Hugo Herbelin
2018-05-22Merge PR #7384: Split UniversesPierre-Marie Pédrot
2018-05-22Merge PR #7324: Infrastructure for ocamldebug on the checkerHugo Herbelin
2018-05-22Merge PR #7526: [circle] Use Docker image from Gitlab registry.Gaëtan Gilbert
2018-05-22Merge PR #7568: [ci] [gitlab] Fix printenv sorting for variables that span mu...Gaëtan Gilbert
2018-05-22Merge PR #6859: [stm] Make toplevels standalone executables.Théo Zimmermann
2018-05-21[ci] [gitlab] Fix printenv sorting for variables that span multiple lines.Emilio Jesus Gallego Arias
2018-05-21Document the new nested-proof error message.Théo Zimmermann
2018-05-21[ide] Remove special option `-ideslave`Emilio Jesus Gallego Arias
2018-05-21[stm] Make toplevels standalone executables.Emilio Jesus Gallego Arias
2018-05-21[ci] Add Dune to the base system.Emilio Jesus Gallego Arias
2018-05-20Merge PR #7557: Add test cases from #7554Théo Zimmermann
2018-05-20Add test cases from #7554Tej Chajed
2018-05-19Merge PR #7527: [windows] Don't build menhir and int anymore in the packaging...Michael Soegtrop
2018-05-18Merge PR #7550: [CI] Fix the script used by math-classes.Emilio Jesus Gallego Arias
2018-05-18Merge PR #6965: [api] Move universe syntax to `Glob_term`Pierre-Marie Pédrot
2018-05-18Clean-up dead file in test-suite.Théo Zimmermann
2018-05-18[CI] Fix the script used by math-classes.Pierre-Marie Pédrot
2018-05-17Split off Universes functions for minimization.Gaëtan Gilbert
2018-05-17Make Universes.refresh_constraints internal to UStateGaëtan Gilbert
2018-05-17Split off Universes functions about substitutions and constraintsGaëtan Gilbert
2018-05-17Remove unused argument to solve_constraints_systemGaëtan Gilbert
2018-05-17Move solve_constraint_system near its only use site (comInductive)Gaëtan Gilbert
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-05-17Split off Universes functions dealing with names.Gaëtan Gilbert
2018-05-17Stop using Universes.subst(_opt)_univs_constrGaëtan Gilbert
2018-05-17Make set minimization option internal to UniversesGaëtan Gilbert
2018-05-17[circle] Use Docker image from Gitlab registry.Emilio Jesus Gallego Arias
2018-05-17Merge PR #7451: Introduce an option to allow nested lemma, and turn it off by...Emilio Jesus Gallego Arias
2018-05-17Merge PR #7359: Reduce usage of evar_map referencesPierre-Marie Pédrot
2018-05-17Merge PR #7449: [vernac] taint two out-of-api `to_constr` use in `comDefiniti...Pierre-Marie Pédrot
2018-05-17Merge PR #6870: [ide] Don't set `quiet` on start.Enrico Tassi
2018-05-17Merge PR #7525: [ci] Try to build more of fiat-crypto.Gaëtan Gilbert
2018-05-17Merge PR #6808: Add unit tests to test-suiteGaëtan Gilbert
2018-05-17Document nested proofs and associated option.Théo Zimmermann
2018-05-17[STM] Nested Proofs Allowed has to be executed immediatelyEnrico Tassi
2018-05-17Remove deprecation warning for nested proofs.Théo Zimmermann
2018-05-17Introduce an option to allow nested lemma, and turn it off by default.Théo Zimmermann
2018-05-16Merge PR #7517: [sphinx] Fix indentation at the end of proof handling chapter.Maxime Dénès
2018-05-16Modify make system to include Makefile.common in the test suiteGaëtan Gilbert
2018-05-16[ci] Try to build more of fiat-crypto.Emilio Jesus Gallego Arias
2018-05-16Merge PR #7514: [ci] Don't build lite versions of CI developments.Gaëtan Gilbert
2018-05-16Merge PR #7535: Typo in documentation of DeriveThéo Zimmermann
2018-05-16Merge PR #7493: Minor update of the documentation about the rcfileEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 17:09:50 +0000