aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2019-02-08Add overlay for EquationsMatthieu Sozeau
2019-02-08Fix issue found in GeoCoqMatthieu Sozeau
2019-02-08Add overlays for unicoq and mtac2Matthieu Sozeau
2019-02-08Add back the deprecated conv/cumul functions.Matthieu Sozeau
2019-02-08Document the unify_flags more throroughly in evarsolve.Matthieu Sozeau
2019-02-08[evarconv] Handle frozen evars in solve_unif_constraints_with_heuristicsMatthieu Sozeau
2019-02-08[evarconv] Clean second order matching of evdrefsMatthieu Sozeau
2019-02-08Change interfaces of evarconv as suggested by Enrico.Matthieu Sozeau
2019-02-08print_constr_env moved to Internal moduleMatthieu Sozeau
2019-02-08Fix warning unused variableMatthieu Sozeau
2019-02-08[occur_rigidly] Try improving occur-check approximationMatthieu Sozeau
2019-02-08Add an helper [instantiate_evar] functionMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-10 18:40:43 +0000