aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-02-13refactor grammarEnrico Tassi
2019-02-13Fix #9432: canonical structure and coercion accept universe binders.Gaëtan Gilbert
2019-02-13Merge PR #9557: [ssreflect] Export more parsing witnesses.Enrico Tassi
2019-02-13Merge PR #9173: [tactics] Remove dependency of abstract on global proof state.Maxime Dénès
2019-02-12Merge PR #9548: Almost fully type-safe gramlib implementationEmilio Jesus Gallego Arias
2019-02-12Merge PR #9563: Improve the documentation of auto.Clément Pit-Claudel
2019-02-12Improve the documentation of auto.Théo Zimmermann
2019-02-12[tactics] Remove dependency of abstract on global proof state.Emilio Jesus Gallego Arias
2019-02-11Merge PR #9551: Small typos in the documentation.Théo Zimmermann
2019-02-11Merge PR #9540: [ssr] keep user annotation on views (fix #9538)Cyril Cohen
2019-02-11[ssreflect] Export more parsing witnesses.Emilio Jesus Gallego Arias
2019-02-11Merge PR #9544: [coqargs] Minor refactoring of error functions.Enrico Tassi
2019-02-11Merge PR #9531: [test-suite] Improve test for async workers.Enrico Tassi
2019-02-11Small typos in the documentation.Martin Bodin
2019-02-11Almost fully type-safe implementation of camlp5.Pierre-Marie Pédrot
2019-02-11Further propagation of well-typedness in Grammar.Pierre-Marie Pédrot
2019-02-11Introduce a GADT of well-typed grammar entries in Grammar.Pierre-Marie Pédrot
2019-02-11Centralizing the calls to the global mutable grammar in Grammar.Pierre-Marie Pédrot
2019-02-11Specialize the intermediate types of the Grammar functor.Pierre-Marie Pédrot
2019-02-11Make Grammar truly functorial.Pierre-Marie Pédrot
2019-02-11Move most of Gramext into Grammar.Pierre-Marie Pédrot
2019-02-11Merge PR #9465: [Nix-CI] Add iris and lambda-rustMaxime Dénès
2019-02-11[coqargs] Minor refactoring of error functions.Emilio Jesus Gallego Arias
2019-02-11Merge PR #9541: [stm] -async-proofs-tac-j accepts only >= 1 (fix #9533)Emilio Jesus Gallego Arias
2019-02-11Merge PR #9543: [ocamldebug] Fix load order after gramlib refactoring.Gaëtan Gilbert
2019-02-11Merge PR #9522: Update link to refman for master branch.Vincent Laporte
2019-02-11[stm] -async-proofs-tac-j accepts only >= 1 (fix #9533)Enrico Tassi
2019-02-11[ssr] keep user annotation on views (fix #9538)Enrico Tassi
2019-02-11[ocamldebug] Fix load order after gramlib refactoring.Emilio Jesus Gallego Arias
2019-02-11Merge PR #9478: Remove the comment fields of locations.Emilio Jesus Gallego Arias
2019-02-11Merge PR #9534: Workaround for CI not having enough RAM for bedrock2: `-async...Emilio Jesus Gallego Arias
2019-02-10Merge PR #9535: [readme] Add link to information about release plans.Théo Zimmermann
2019-02-10Merge PR #9536: [ci] Remove unused bintray file.Maxime Dénès
2019-02-09remove `allow_failure: true` for bedrock2Samuel Gruetter
2019-02-09remove VERBOSE=1, gitlab log shows that `-async-proofs-tac-j 1` was indeed pa...Samuel Gruetter
2019-02-09Update link to refman and stdlib doc for master branch.Théo Zimmermann
2019-02-09[ci] Remove unused bintray file.Emilio Jesus Gallego Arias
2019-02-09[readme] Add link to information about release plans.Emilio Jesus Gallego Arias
2019-02-08Workaround for CI not having enough RAM for bedrock2: `-async-proofs-tac-j 1`Samuel Gruetter
2019-02-08Merge PR #9525: Remove global output_native_objects flag.Emilio Jesus Gallego Arias
2019-02-08Merge PR #9523: Make boot flag into a normal option (no global flag).Emilio Jesus Gallego Arias
2019-02-08[test-suite] Improve test for async workers.Emilio Jesus Gallego Arias
2019-02-08Merge PR #9481: [parsing] Use AST node for main parsing entry.Enrico Tassi
2019-02-08Merge PR #9492: [stm] Filter some more arguments that shouldn't be sent to wo...Enrico Tassi
2019-02-08Merge PR #9504: Add print_pure_econstr signatureGaëtan Gilbert
2019-02-08coqargs: use algebraic datatype for -native-compilerGaëtan Gilbert
2019-02-08Remove global output_native_objects flag.Gaëtan Gilbert
2019-02-08Make boot flag into a normal option (no global flag).Gaëtan Gilbert
2019-02-08Merge PR #9513: Edit release-process.md to ease upcoming releases of Coq in D...Théo Zimmermann
2019-02-08[stm] Filter some more arguments that shouldn't be sent to workers.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-21 03:03:55 +0000