aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-07-19Remove declare_object for SsrHave NoTCResolution.Maxime Dénès
2018-07-18Merge PR #8054: [dev] Autogenerate OCaml dev files.Enrico Tassi
2018-07-18Merge PR #7897: Remove fourier pluginEnrico Tassi
2018-07-18Merge PR #8068: [build] Build Coq and plugins with `-strict-sequence`Enrico Tassi
2018-07-18Merge PR #8060: Remove useless libobject in proof_usingEnrico Tassi
2018-07-17Merge PR #8055: Fast accumulator check in native compilationMaxime Dénès
2018-07-17Remove fourier pluginMaxime Dénès
2018-07-17change into QuestionMark defaultSiddharth Bhat
2018-07-17Add overlay for Coq-Equations for QuestionMark.Siddharth Bhat
2018-07-17Change QuestionMark for better record field missing error message.Siddharth Bhat
2018-07-16Mention the automatic use of the rebase label.Théo Zimmermann
2018-07-16Move long label links to the bottom of CONTRIBUTING.mdThéo Zimmermann
2018-07-16Restrict universes in comInductiveJasper Hugunin
2018-07-16Merge PR #8069: Only check overlay extensions on git-tracked filesGaëtan Gilbert
2018-07-16Add overlay for QuickChickJason Gross
2018-07-16Update CHANGESJason Gross
2018-07-16Add additional lemmas about {String,Ascii}.eqbJason Gross
2018-07-16Add Extract Inlined Constant directives for {String,Ascii}.eqbJason Gross
2018-07-16Ascii.eqb and String.eqbPierre Letouzey
2018-07-16bin,oct,hex conversions positive,Z,N,nat<->stringJason Gross
2018-07-16Only check overlay extensions on git-tracked filesJason Gross
2018-07-16Fix #7291: unify tactic should have more descriptive error messages.Pierre-Marie Pédrot
2018-07-16Merge PR #8023: Introduce a team of code owners for the CI system.Maxime Dénès
2018-07-16Merge PR #8066: [ltac] Remove unused functions.Pierre-Marie Pédrot
2018-07-15Use GitHub as the location for OCaml sources.Théo Zimmermann
2018-07-14[build] Build Coq and plugins with `-strict-sequence`Emilio Jesus Gallego Arias
2018-07-14[ltac] Remove unused functions / constructors.Emilio Jesus Gallego Arias
2018-07-13Merge PR #8057: Fixed typos, wording and grammar errors in the Preamble of th...Théo Zimmermann
2018-07-13Remove useless libobject in proof_usingMaxime Dénès
2018-07-13Merge PR #6930: Make -warn-error fail on warnings emitted by coqc on stdlib.Emilio Jesus Gallego Arias
2018-07-13Make -warn-error fail on warnings emitted by coqc on stdlib.Maxime Dénès
2018-07-13Generate type-specific code for is_accu in native compilation of fixpoints.Pierre-Marie Pédrot
2018-07-13Store the {struct} inductive type in native fixpoint AST.Pierre-Marie Pédrot
2018-07-13Pass a proper environment to Nativelambda.lambda_of_constr.Pierre-Marie Pédrot
2018-07-12Fixed typos, wording and grammar errors in the Preamble of the Reference Manu...Zeimer
2018-07-12Merge PR #8041: [ci] Remove warning jobs in favor of default `-warn-error yes`Gaëtan Gilbert
2018-07-12Merge PR #7907: Tactic deprecation machineryPierre-Marie Pédrot
2018-07-12[dev] Autogenerate OCaml dev files.Emilio Jesus Gallego Arias
2018-07-12Merge PR #8051: Clean-up user-overlays folder.Emilio Jesus Gallego Arias
2018-07-12Clean-up user-overlays folder.Théo Zimmermann
2018-07-12[warnings] Disable warning 58 "no cmx file was found in path"Emilio Jesus Gallego Arias
2018-07-12[warnings] Disable warning 59 [assignment to a non-mutable value] to make fla...Emilio Jesus Gallego Arias
2018-07-12Fix #7854: Native compilation + flambda trigger SEGFAULT.Pierre-Marie Pédrot
2018-07-12[ci] Remove warning jobs in favor of default `-warn-error yes`Emilio Jesus Gallego Arias
2018-07-12Cleanup reduction effects: they only work on constants.Gaëtan Gilbert
2018-07-12Statically typecheck the VERNAC EXTEND wrapper.Pierre-Marie Pédrot
2018-07-12Export a wrapper simplifying the registration of vernacular commands.Pierre-Marie Pédrot
2018-07-12Merge PR #7871: [ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0Gaëtan Gilbert
2018-07-12Tactic deprecation machineryMaxime Dénès
2018-07-11[ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0Emilio Jesus Gallego Arias