aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-02-08Rename types_or_terms and the unification function typesMatthieu Sozeau
2019-02-08Fix indentation (removing tabs)Matthieu Sozeau
2019-02-08Correct occur_rigidlyMatthieu Sozeau
2019-02-08Abstraction namingMatthieu Sozeau
2019-02-08unification: abstract_list_all_with_dependencies fixMatthieu Sozeau
2019-02-08evarconv/evarsolve: HO matching algorithm with occurrence selectionMatthieu Sozeau
2019-02-08[evarconv] New flag handling for unifierMatthieu Sozeau
2019-02-08locus: Add an AtLeastOneOccurrence constructor.Matthieu Sozeau
2019-02-08Evd/evarsolve: add an abstraction field to evars for unificationMatthieu Sozeau
2019-02-08Merge PR #9410: Make `Program` a regular attributeMatthieu Sozeau
2019-02-08Merge PR #9515: [Gitlab-CI] Automatic deployment of the standard library docu...Emilio Jesus Gallego Arias
2019-02-08[Gitlab-CI] Automatic deployment of the standard library documentation to GH-...Vincent Laporte
2019-02-07Merge PR #9499: [Gitlab-CI] Never attempt to build cachixThéo Zimmermann
2019-02-07Merge PR #9477: Makefiles: Fixes for byte compilationEnrico Tassi
2019-02-07Merge PR #9475: Automatic deployment of the user manual to GH-PagesGaëtan Gilbert
2019-02-07[Gitlab-CI] Never attempt to build cachixVincent Laporte
2019-02-07Merge PR #9496: Avoid eqn when generating name in induction_gen.Pierre-Marie Pédrot
2019-02-07Merge PR #9498: [dune] Fix OCaml trunk build.Gaëtan Gilbert
2019-02-07Merge PR #9479: Remove the Plexing.Error exception.Emilio Jesus Gallego Arias
2019-02-07[dune] Fix OCaml trunk build.Emilio Jesus Gallego Arias
2019-02-06[Gitlab-CI] Deploy manual to GH-PagesVincent Laporte
2019-02-06Avoid eqn when generating name in induction_gen.Jasper Hugunin
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-06Makefiles: Fixes for byte compilationGaëtan Gilbert
2019-02-06Merge PR #9487: Fix #9281: forgotten CeCILL-B headers in ssrmatching plugin.Enrico Tassi
2019-02-06Fix #9486: Makefile.install should not have a target fooGaëtan Gilbert
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-05Remove the Plexing.Error exception.Pierre-Marie Pédrot
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-05OverlaysMaxime Dénès
2019-02-05Make Program a regular attributeMaxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 18:18:30 +0000