aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-09-18Merge PR #8485: Missing space in cic.rstThéo Zimmermann
2018-09-17Merge PR #6906: [VM] Optimize structured valuesPierre-Marie Pédrot
2018-09-17Merge PR #8053: [dune] Add apidoc target using `odoc`Gaëtan Gilbert
2018-09-17OCaml now exports the min and max non-constant tags, let's use itMaxime Dénès
2018-09-17Add assertion on tags in eq_structured_constantsMaxime Dénès
2018-09-17[VM] Allocate a bit less in digits_from_uintMaxime Dénès
2018-09-17[VM] Inject structured constants in values without reallocating them.Maxime Dénès
2018-09-17[VM] Move structured_constant to VmvaluesMaxime Dénès
2018-09-16Missing space in cic.rstJoachim Breitner
2018-09-14Merge PR #7894: Remove quote pluginThéo Zimmermann
2018-09-14Merge PR #8326: Mention PRINT_LOGS=1 when failing test suiteEnrico Tassi
2018-09-13Merge PR #8434: Canonical representation of kernel substitutionsMaxime Dénès
2018-09-13Merge PR #8436: Move maps & sets indexed by GlobRef.t into the kernelMaxime Dénès
2018-09-13Merge PR #8303: Better controls for template polymorphismMaxime Dénès
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 07:17:23 +0000