aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-16Mising prime in the subtyping rulesJoachim Breitner
2018-09-16Missing space in cic.rstJoachim Breitner
2018-09-15Overlay for cross-crypto.Hugo Herbelin
2018-09-14Fixing yet a source of dependency on alphabetic order in unification.Hugo Herbelin
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-14Register: simpler syntaxVincent Laporte
2018-09-14Retroknowledge: use GlobRef.t instead of Constr.t as entryVincent Laporte
2018-09-14Retroknowledge: simpler parsing rulesVincent Laporte
2018-09-14Retroknowledge: remove the (unused) by clauseVincent Laporte
2018-09-14Retroknowledge.KInt31: remove the (unused) group parameterVincent Laporte
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 entry for universe polymorphism critical bugGaëtan Gilbert
2018-09-13Add test for inconsistency from polymorphism capturing global univsGaëtan Gilbert
2018-09-13Do not catch already declared universes in Environ.add_universesGaëtan Gilbert
2018-09-13Avoid repeat univ declaration in cumulative subtyping checkGaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-13 12:56:59 +0000