aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-10-23Order Greek letters consistently w/rest of documentSam Pablo Kuper
2018-10-23[dune] Compile debug and checker printers.Emilio Jesus Gallego Arias
2018-10-23[build] Refactoring to config lib and ocamldebug tweaks.Emilio Jesus Gallego Arias
2018-10-22[doc] [api] Update `odoc` to new release 1.3.0Emilio Jesus Gallego Arias
2018-10-22Merge PR #8708: Stupid but critical unfolding heuristic.Maxime Dénès
2018-10-22Merge PR #8784: [dune] Remove rule for cLexer.ml4 -> cLexer.mlThéo Zimmermann
2018-10-21Adding a regression test for bug #8785 (missing univ constraints registration).Hugo Herbelin
2018-10-20Merge PR #8769: [library] Remove redundant re-addition of universe constraints.Gaëtan Gilbert
2018-10-20[dune] Remove rule for cLexer.ml4 -> cLexer.mlEmilio Jesus Gallego Arias
2018-10-20Merge PR #8782: gitignore test-suite/.nia.cacheThéo Zimmermann
2018-10-19Merge PR #8758: [api] Qualify access to `Nametab`Hugo Herbelin
2018-10-19gitignore test-suite/.nia.cacheGaëtan Gilbert
2018-10-19Deprecating unused Engine.type_of_global.Hugo Herbelin
2018-10-19Deprecating Global.type_of_global_in_context.Hugo Herbelin
2018-10-19Deprecating Global.constr_of_global_in_context.Hugo Herbelin
2018-10-19Moving Global.constr_of_global_in_context to Typeops.Hugo Herbelin
2018-10-19Moving Global.type_of_global_in_context to Typeops.Hugo Herbelin
2018-10-19Cleaning layout typeops.mli.Hugo Herbelin
2018-10-19Porting the test-suite to coqpp.Pierre-Marie Pédrot
2018-10-19Adapt coq_makefile to handle coqpp-based macro files.Pierre-Marie Pédrot
2018-10-19Merge PR #8724: [universes] deprecate constr_of_globalPierre-Marie Pédrot
2018-10-19Explicitly merge contexts in side-effect universe handling.Pierre-Marie Pédrot
2018-10-19Move side-effect typing into Safe_env.Pierre-Marie Pédrot
2018-10-19Merge PR #8740: Removing the Camlp5 macros from CLexer.Emilio Jesus Gallego Arias
2018-10-19Replace non-idiomatic "dead-alleys" with idiomatic "dead-ends"Sam Pablo Kuper
2018-10-18[library] Remove redundant re-addition of universe constraints.Emilio Jesus Gallego Arias
2018-10-18Merge PR #8719: [ci] [appveyor] Disable validate target.Maxime Dénès
2018-10-18Merge PR #8670: Document the issue with positive coinductive types.Théo Zimmermann
2018-10-18Adding a rule to generate grammar.cma.Pierre-Marie Pédrot
2018-10-18Removing the Camlp5 macros from CLexer.Pierre-Marie Pédrot
2018-10-18[universes] deprecate constr_of_globalMatthieu Sozeau
2018-10-18[api] Qualify access to `Nametab`Emilio Jesus Gallego Arias
2018-10-18Merge PR #8761: [ci] Pin CI_REF to plugin_tutorial to use not yet merged commit.Emilio Jesus Gallego Arias
2018-10-18[ci] Pin CI_REF to plugin_tutorial to use not yet merged commit.Théo Zimmermann
2018-10-18Merge PR #8756: [micromega] Build csdpcertVincent Laporte
2018-10-18Merge PR #8754: [doc] [build] Remove ocamlbuild leftovers.Théo Zimmermann
2018-10-17doc: mention ByteVectorYishuai Li
2018-10-17Strings: add ByteVectorYishuai Li
2018-10-17[micromega] Build csdpcertEmilio Jesus Gallego Arias
2018-10-17[doc] [build] Remove ocamlbuild leftovers.Emilio Jesus Gallego Arias
2018-10-17Merge PR #8694: Various cleanups of universe apisPierre-Marie Pédrot
2018-10-17Merge PR #8710: [omega, btauto] Remove some dead codePierre-Marie Pédrot
2018-10-17Merge PR #8748: [dune] [plugins] Fix plugin name ground -> firstorderThéo Zimmermann
2018-10-17[dune] [plugins] Fix plugin name ground -> firstorderEmilio Jesus Gallego Arias
2018-10-16Merge PR #8738: [clib] Deprecate string functions available in OCaml 4.05Pierre-Marie Pédrot
2018-10-16Merge PR #8742: [clib] Remove Array functions available in OCaml 4.05.0Pierre-Marie Pédrot
2018-10-16Merge PR #8059: Simplify code for [Definition := Eval ...]Matthieu Sozeau
2018-10-16{Univops->UState}.restrict_universe_contextGaëtan Gilbert
2018-10-16{Univops -> Vars}.universes_of_constrGaëtan Gilbert
2018-10-16UnivGen.extend_context -> Univ.extend_in_context_setGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 23:15:28 +0000