aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-11Fix #9508: Unexpected interaction between implicit arguments and primitive pr...Pierre-Marie Pédrot
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-11Fix #9527: unknown evar in nonterminating [fix] error.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[coqdoc] Add the From keywordPierre Roux
2019-02-11Use math mode more.Tanaka Akira
2019-02-11Use {LEFT,RIGHT} DOUBLE QUOTATION MARK.Tanaka Akira
2019-02-11Remove a space before closing double-quote.Tanaka Akira
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-10Change "I" to "I_p".Tanaka Akira
2019-02-10Distinguish inductive {definition,inductive}.Tanaka Akira
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[coq] Adapt to coq/coq#9137Emilio Jesus Gallego Arias
2019-02-09[readme] Add link to information about release plans.Emilio Jesus Gallego Arias
2019-02-09Merge pull request coq/ltac2#102 from maximedenes/rm-unknownPierre-Marie Pédrot
2019-02-08Workaround for CI not having enough RAM for bedrock2: `-async-proofs-tac-j 1`Samuel Gruetter
2019-02-08Remove VtUnknown classificationMaxime Dénès
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-08Change Primitive message: "is registered" -> "is declared".Gaëtan Gilbert
2019-02-08Update overlay fileMatthieu Sozeau
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 pull request coq/ltac2#101 from maximedenes/program-mode-flagPierre-Marie Pédrot
2019-02-08Merge PR #9513: Edit release-process.md to ease upcoming releases of Coq in D...Théo Zimmermann
2019-02-08evarsolve transp_state and comments fixesMatthieu Sozeau
2019-02-08evarconf transp state and comments fixesMatthieu Sozeau
2019-02-08Coercion intf fixMatthieu Sozeau