aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2018-09-19Fix #7754: universe declarations on mutual inductivesGaëtan Gilbert
2018-09-19Merge PR #8341: Reduce universe redeclarations (catching AlreadyDeclared)Matthieu Sozeau
2018-09-14Register: simpler syntaxVincent Laporte
2018-09-14Retroknowledge: use GlobRef.t instead of Constr.t as entryVincent Laporte
2018-09-13Merge PR #8436: Move maps & sets indexed by GlobRef.t into the kernelMaxime Dénès
2018-09-13Do not redeclare universes for monomorphic operational typeclassesGaë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-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-12Move maps & sets indexed by GlobRef.t into the kernelVincent Laporte
2018-09-12Merge PR #8433: Fix bug #8432 : program fixpoint and universesPierre-Marie Pédrot
2018-09-11Merge PR #7135: Introducing an explicit `Declare Scope` commandEmilio Jesus Gallego Arias
2018-09-10Remove environment passing to coercion printersGaëtan Gilbert
2018-09-10Merge PR #8417: Fixing #8416: Print Assumptions missing module information fr...Matthieu Sozeau
2018-09-10Support for Local flag in Declare Scope, Undelimit/Delimit Scope, Bind Scope.Hugo Herbelin
2018-09-10Adding a command "Declare Scope" and deprecating scope implicit declaration.Hugo Herbelin
2018-09-07Fix bug #8432 : program fixpoint and universesMatthieu Sozeau
2018-09-06Merge PR #8295: Fix #8291: print universe names in universe context for Check.Matthieu Sozeau
2018-09-05Fixing #8416 (Print Assumptions missing module information from compiled files).Hugo Herbelin
2018-09-05Merge PR #6857: [build] Preliminary support for building with `dune`.Théo Zimmermann
2018-09-05Merge PR #7968: Restrict universes in comInductiveGaëtan Gilbert
2018-09-05[build] Preliminary support for building Coq with `dune`.Emilio Jesus Gallego Arias
2018-09-03Merge PR #891: Check universes are declaredGaëtan Gilbert
2018-09-03Merge PR #7912: Simplify effects APIMaxime Dénès
2018-09-03Merge PR #7085: Turn the kernel reduction sharing flag into an argument passe...Maxime Dénès
2018-08-28Close #8091: print universe context for Eval when option on.Gaëtan Gilbert
2018-08-28Fix #8291: print universe names in universe context for Check.Gaëtan Gilbert
2018-08-27Add support for focusing on named goals using brackets.Théo Zimmermann
2018-08-22Fix #8251: remove "the the" occurrencesGaëtan Gilbert
2018-08-17Remove dead argument allow_old.Théo Zimmermann
2018-07-29Store marshallable data in the custom entry summary.Pierre-Marie Pédrot
2018-07-29Supporting locality flag for custom entries + compatibility with modules.Hugo Herbelin
2018-07-29Do not treat curly brackets specially in custom entries.Hugo Herbelin
2018-07-29Renaming ETName and ETReference so as to fit the user-visible terminology.Hugo Herbelin
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-07-26Turn the kernel reduction sharing flag into an argument passed in the cache.Pierre-Marie Pédrot
2018-07-26Merge PR #8050: Cleanup VERNAC EXTENDMaxime Dénès
2018-07-26Merge PR #7786: In "redundant clause" pattern-matching error, show also the p...Pierre-Marie Pédrot
2018-07-25In "redundant clause" pattern-matching error, show also the pattern (#7777).Hugo Herbelin
2018-07-25kernel: missing check that all universes are declared.Matthieu Sozeau
2018-07-25Remove himsg.pr_puniverses, use @{} for universe printing in errorsMaxime Dénès
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-23Displays the differences between successive proof steps in coqtop and CoqIDE.Jim Fehrle
2018-07-23Generate more compact escape sequences byJim
2018-07-19Merge PR #7941: Extend QuestionMark to produce a better error message in case...Pierre-Marie Pédrot
2018-07-17change into QuestionMark defaultSiddharth Bhat
2018-07-17Change QuestionMark for better record field missing error message.Siddharth Bhat
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 08:54:10 +0000