aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-09-13Avoid repeat universe declarations for constants with split univsGaëtan Gilbert
2018-09-13Do not redeclare universes for monomorphic operational typeclassesGaëtan Gilbert
2018-09-13Add doc for template polymorphism option and attributes.Gaëtan Gilbert
2018-09-13Add option to control automatic template polymorphism.Gaëtan Gilbert
2018-09-13Add explicit atribute for template polymorphism.Gaëtan Gilbert
2018-09-13Kernel: fully obey mind_entry_templateGaëtan Gilbert
2018-09-13Elaboration: do not ask for small records to be templateGaëtan Gilbert
2018-09-13Elaboration: do not ask poly inductives to be templateGaëtan Gilbert
2018-09-13Elaboration: do not ask small inductives to be templateGaëtan Gilbert
2018-09-13Small simplification of elaboration side of template poly inductivesGaëtan Gilbert
2018-09-13Mention PRINT_LOGS=1 when failing test suiteGaëtan Gilbert
2018-09-13Move test suite report script to standalone script fileGaëtan Gilbert
2018-09-13Merge PR #8467: Manual: fix documentation of the “fresh” tacticThéo Zimmermann
2018-09-13Merge PR #8470: Fix mli-doc following #7109.Maxime Dénès
2018-09-12Fix mli-doc following #7109.Théo Zimmermann
2018-09-12Move maps & sets indexed by GlobRef.t into the kernelVincent Laporte
2018-09-12Merge PR #8097: Use more efficient accu check for cofix unfolding in native c...Maxime Dénès
2018-09-12Merge PR #7109: Term combinators respecting the canonical structure of branch...Maxime Dénès
2018-09-12Remove quote pluginMaxime Dénès
2018-09-12Manual: fix documentation of the “fresh” tacticVincent Laporte
2018-09-12Merge PR #8243: Remove xargs from "make clean" so it won't fail on CygwinEnrico Tassi
2018-09-12Merge PR #8433: Fix bug #8432 : program fixpoint and universesPierre-Marie Pédrot
2018-09-12Merge PR #8372: Grammar rule in the documentation of ssreflect's anonymous ar...Théo Zimmermann
2018-09-12Merge PR #8406: building-a-coq-project-with-coq-makefile:fix typosThéo Zimmermann
2018-09-11Merge PR #8444: Bump version number to 8.10+alpha.Emilio Jesus Gallego Arias
2018-09-11building-a-coq-project-with-coq-makefile:fix typosJason Gross
2018-09-11Made names of existential variables interpretable as Ltac variables.Hugo Herbelin
2018-09-11Merge PR #7288: Isolating ltac naming out of pretyping + fixing renamingPierre-Marie Pédrot
2018-09-11Merge PR #8285: Fixing #8270: cbn was applying zeta even when not asked for.Pierre-Marie Pédrot
2018-09-11Merge PR #8278: Do not inline let-bound functions in clambda optimization.Maxime Dénès
2018-09-11Merge PR #8284: [ssr] anomaly -> errorMaxime Dénès
2018-09-11Grammar entry for the ssr syntax for anonymous arguments.Assia Mahboubi
2018-09-11Merge PR #8425: Deprecate romega in favor of liaPierre-Marie Pédrot
2018-09-11Merge PR #7135: Introducing an explicit `Declare Scope` commandEmilio Jesus Gallego Arias
2018-09-11Merge PR #8452: Fix #8358: circular make dependency for camldevfilesEnrico Tassi
2018-09-11Merge PR #8448: Have `gitFull` in the nix-shellVincent Laporte
2018-09-11Merge PR #8105: Remove environment passing to cache_coercion functionHugo Herbelin
2018-09-10Remove environment passing to coercion printersGaëtan Gilbert
2018-09-10Merge PR #8230: fix formulation of the Euclid Theorem in commentHugo Herbelin
2018-09-10Declaring Scope prior to loading primitive printers.Hugo Herbelin
2018-09-10Documenting "Declare Scope".Hugo Herbelin
2018-09-10CHANGES: mentioning new command "Declare Scope".Hugo Herbelin
2018-09-10Fix #8358: circular make dependency for camldevfilesGaëtan Gilbert
2018-09-10Have `gitFull` in the nix-shellCyril Cohen
2018-09-10Merge PR #8417: Fixing #8416: Print Assumptions missing module information fr...Matthieu Sozeau
2018-09-10Merge PR #8290: Fix #8288: cumulativity inferance ignores args to bound varia...Matthieu Sozeau
2018-09-10Merge PR #7743: Bound proof-search in default program obligation tactic.Pierre-Marie Pédrot
2018-09-10Merge PR #8323: Owners of Makefile.{ci,doc} are teams {ci,doc}-maintainers.Maxime Dénès
2018-09-10Merge PR #8430: Move to a team of code owners for the Nix files.Maxime Dénès
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 22:51:57 +0000