aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-02-08Remove spaces just before period (non-math mode).Tanaka Akira
2019-02-08Remove spaces just before comma (non-math mode).Tanaka Akira
2019-02-08Remove "'" accidentaly added.Tanaka Akira
2019-02-06Merge PR #9124: Document the possibility of declaring a Ltac name_goal.Clément Pit-Claudel
2019-02-06Merge PR #9456: The lowest universe level is 1.Théo Zimmermann
2019-02-06Document the possibility of declaring a Ltac name_goal.Théo Zimmermann
2019-02-06Merge PR #9487: Fix #9281: forgotten CeCILL-B headers in ssrmatching plugin.Enrico Tassi
2019-02-06Fix #9281: forgotten CeCILL-B headers in ssrmatching plugin.Théo Zimmermann
2019-02-05Merge PR #9397: Simplify code for Recordops.cs_pattern_of_constrMatthieu Sozeau
2019-02-05Merge PR #9472: Add advice and an example to the documentation of fold.Clément Pit-Claudel
2019-02-05Merge PR #9373: Kernel: don't automatically downgrade ill-shaped primitive re...Pierre-Marie Pédrot
2019-02-05Merge PR #9438: Cleanup universe length for inductives in vconvPierre-Marie Pédrot
2019-02-05Merge PR #9396: Skip indirection through Evd for obligation ustate manipulationMatthieu Sozeau
2019-02-05Merge PR #8421: [dune] Fix Dune build in Windows.Théo Zimmermann
2019-02-05Add advice and an example to the documentation of fold.Théo Zimmermann
2019-02-04Merge PR #9470: the default branch of Mtac2 changed to masterEmilio Jesus Gallego Arias
2019-02-04Merge PR #9468: Remove AppVeyor: superseded by Azure.Emilio Jesus Gallego Arias
2019-02-04the default branch of Mtac2 changed to masterbeta
2019-02-04[dune] Fix Dune build in Windows.Emilio Jesus Gallego Arias
2019-02-04Remove AppVeyor: superseded by Azure.Théo Zimmermann
2019-02-04Merge PR #6914: Primitive integersPierre-Marie Pédrot
2019-02-04Merge PR #9317: Restrict universes in records.Pierre-Marie Pédrot
2019-02-04Merge PR #9144: Fixes #4633: clearer message unknown existentialPierre-Marie Pédrot
2019-02-04Merge PR #9409: Move non-primitive-record warning to declare_mutual_inductive...Pierre-Marie Pédrot
2019-02-04Merge PR #9437: Comment universe operations in Classes.contextPierre-Marie Pédrot
2019-02-04Merge PR #9386: Pass some files to strict focusing mode.Pierre-Marie Pédrot
2019-02-04Overlays.Maxime Dénès
2019-02-04Primitive integersMaxime Dénès
2019-02-04Dockerfile: update menhir from 20180530 to 20181113Vincent Laporte
2019-02-04Merge PR #9368: Discard argument names of section variables on section closePierre-Marie Pédrot
2019-02-04Merge PR #8690: [toplevel] Split interactive toplevel and compiler binaries.Maxime Dénès
2019-02-04Merge PR #9426: [test-suite] Fix display of check.Enrico Tassi
2019-02-04Merge PR #9454: Fix off-by-one error in nat syntax warningsPierre-Marie Pédrot
2019-02-04Merge PR #9452: [proof] optimize proof always works on incomplete proofsPierre-Marie Pédrot
2019-02-04Merge PR #9461: Fix default goal selector error message.Pierre-Marie Pédrot
2019-02-04Merge PR #9291: Do not take universes into account in lia reification.Frédéric Besson
2019-02-02Merge PR #9250: coqchk: fix check for kelim with functorsPierre-Marie Pédrot
2019-02-02Merge PR #9395: Global [open Univ] in UStatePierre-Marie Pédrot
2019-02-01Fix default goal selector error message.Gaëtan Gilbert
2019-02-01Merge PR #8062: Add Z.div_mod_to_quot_rem tactic, put it in zifyVincent Laporte
2019-02-01[toplevel] Split interactive toplevel and compiler binaries.Emilio Jesus Gallego Arias
2019-02-01Merge PR #9415: Simplify the GitHub issue templateMaxime Dénès
2019-02-01Merge PR #9095: [toplevel] Deprecate `-compile` flag in favor of `coqc`Maxime Dénès
2019-02-01The lowest universe level is 1.Tanaka Akira
2019-01-31Fix off-by-one error in nat syntax warningsJason Gross
2019-01-31add testEnrico Tassi
2019-01-31[proof] optimize proof always works on incomplete proofsEnrico Tassi
2019-01-31Merge PR #9449: Fix small errors in cic.rst (2nd).Théo Zimmermann
2019-01-31Merge PR #9448: [ci] [ocaml] Fix OCaml trunk builds.Gaëtan Gilbert
2019-01-31Use λ instead of \lb.Tanaka Akira