aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-19Merge PR #8740: Removing the Camlp5 macros from CLexer.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-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-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
2018-10-16Deprecate UnivGen.new_{univ,Type,Type_sort}Gaëtan Gilbert
2018-10-16Clean UnivGen.fresh_instance APIGaëtan Gilbert
2018-10-16Deprecate univ-dropping UnivGen.new_sort_in_familyGaëtan Gilbert
2018-10-16Simplify UnivGen.type_of_referenceGaëtan Gilbert
2018-10-16UnivGen.constr_of_glob_univ -> Constr.mkRefGaëtan Gilbert
2018-10-16Remove [constr_of_global_in_context] in funindGaëtan Gilbert
2018-10-16Simplify vars_of_global usageGaëtan Gilbert
2018-10-16Simplify fresh_foo_instance functions and pretyping of univ instanceGaëtan Gilbert
2018-10-16Deprecate Global.universes_of_global (replaced by environ version)Gaëtan Gilbert
2018-10-16[Omega] Remove dead codeVincent Laporte
2018-10-16[btauto] Remove dead codeVincent Laporte
2018-10-16[omega] Remove dead codeVincent Laporte
2018-10-16Merge PR #8691: Remove some dead code in nsatz and micromega pluginsthery
2018-10-16[clib] Remove Array functions available in OCaml 4.05.0Emilio Jesus Gallego Arias
2018-10-16[clib] Deprecate string functions available in OCaml 4.05Emilio Jesus Gallego Arias
2018-10-16[test-suite] Update csdp cacheVincent Laporte
2018-10-16[micromega] remove dead codeVincent Laporte
2018-10-16[nsatz] remove dead codeVincent Laporte
2018-10-16Document the issue with positive coinductive types.Pierre-Marie Pédrot
2018-10-16Merge PR #8695: Adding a functional version of constant- and mind_of_delta_kn...Pierre-Marie Pédrot
2018-10-16Merge PR #8733: Implement ARGUMENT EXTEND in coqppEmilio Jesus Gallego Arias
2018-10-15Documenting the transition from camlp5 to coqpp for ARGUMENT EXTEND.Pierre-Marie Pédrot
2018-10-15Port remaining EXTEND ml4 files to coqpp.Pierre-Marie Pédrot
2018-10-15Implement ARGUMENT EXTEND in coqpp.Pierre-Marie Pédrot
2018-10-15Plug ARGUMENT EXTEND into the argument extension API.Pierre-Marie Pédrot
2018-10-15Providing a centralized API for ARGUMENT EXTEND.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 23:51:00 +0000