aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-09-17[VM] Move structured_constant to VmvaluesMaxime Dénès
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
Imitating the kernel in anticipation for the kernel being more obedient
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
This doesn't change behaviour currently as the kernel also makes this decision, but in the future it won't.
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
It seems people don't always look at the test suite readme.
2018-09-13Move test suite report script to standalone script fileGaëtan Gilbert
This allows for nicer formatting without having to deal with Make's semantic whitespace.
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 ↵Maxime Dénès
compilation.
2018-09-12Merge PR #7109: Term combinators respecting the canonical structure of ↵Maxime Dénès
branches and return predicate
2018-09-12Remove quote pluginMaxime Dénès
As far as I know, this plugin is untested and barely maintained. I don't think it has real use cases any more, so let's move it out from the repo and see if somebody wants to take over and maintain it. We also remove the documentation, which was telling our users to look at ring to see an example of reification done using quote, when in fact it wasn't using it anymore.
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 ↵Théo Zimmermann
arguments
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
make make-pretty-timed- after -> make make-pretty-timed-after (remove space between - and after) (and reflow paragraph) Fix spacing around :: in print-pretty-single-time-diff Closes #8396
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
(It's unused after moving coercions to globrefs)
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 ↵Matthieu Sozeau
from compiles files
2018-09-10Merge PR #8290: Fix #8288: cumulativity inferance ignores args to bound ↵Matthieu Sozeau
variables
2018-09-10Merge PR #7743: Bound proof-search in default program obligation tactic.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:03:42 +0000