aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-07-29Do not treat curly brackets specially in custom entries.Hugo Herbelin
2018-07-29Classify "Declare Custom" as VtNow for the stm.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-29A test on the different ways to indicate the levels of a rule.Hugo Herbelin
2018-07-29Synchronizing "grammars by name" with backtrack (custom entries shall be adde...Hugo Herbelin
2018-07-28Merge PR #8077: Fix #7291: unify tactic should have more descriptive error me...Hugo Herbelin
2018-07-28Merge PR #8160: Improved chapters 'Implicit Coercions' and 'Canonical Structu...Théo Zimmermann
2018-07-28Merge PR #8148: Doc: preliminary work before #7291 which add an "Unable to un...Théo Zimmermann
2018-07-27Merge PR #8174: [ci] Remove CircleCI setup.Gaëtan Gilbert
2018-07-27Merge PR #8173: Missing backslash in a documentation file.Théo Zimmermann
2018-07-27[ci] Remove CircleCI setup.Emilio Jesus Gallego Arias
2018-07-27Missing backslash in the documentation file.Martin Bodin
2018-07-27Merge PR #8164: Add information to option type errorsEnrico Tassi
2018-07-27Merge PR #8166: Fix Search query in CoqIDE.Enrico Tassi
2018-07-27Merge PR #8103: Coercions cleanup: use GlobRef.t instead of constrEnrico Tassi
2018-07-27Merge PR #8141: Diff option in CoqIDEEnrico Tassi
2018-07-26[sphinx] Do name cleanup in handle_signatureClément Pit-Claudel
2018-07-26NArith: add sized N2BvYishuai Li
2018-07-26Merge PR #8101: Remove ClosedModule and ClosedSection from libstackEnrico Tassi
2018-07-26Fix Search query in CoqIDE.Pierre-Marie Pédrot
2018-07-26Improved chapters 'Implicit Coercions' and 'Canonical Structures' of the Refe...Zeimer
2018-07-26Add information to option type errorsTej Chajed
2018-07-26Replace iter + ref by fold_leftMaxime Dénès
2018-07-26restore reduction of coercion to eventually expose a constructorEnrico Tassi
2018-07-26Coercions cleanup: use GlobRef.t instead of constrMaxime Dénès
2018-07-26Don't use an object for polymorphic section universesGaëtan Gilbert
2018-07-26Universe object is DisposeGaëtan Gilbert
2018-07-26Merge PR #8100: Use just one object declaration for all global universe addit...Pierre-Marie Pédrot
2018-07-26Fix #8121: anomalies in native_compute with let and evars.Pierre-Marie Pédrot
2018-07-26Adding an overlay for Mtac2.Pierre-Marie Pédrot
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-26Expose the diff printing option as an UI entry in CoqIDE.Pierre-Marie Pédrot
2018-07-26Do not set diff printing on by default in CoqIDE.Pierre-Marie Pédrot
2018-07-26Merge PR #8122: Fix #8119: anomalies in vm_compute with let and evars.Maxime Dénès
2018-07-26Merge PR #7786: In "redundant clause" pattern-matching error, show also the p...Pierre-Marie Pédrot
2018-07-26Merge PR #8084: Properly disable native compilation when -native-compiler is ...Maxime Dénès
2018-07-26Merge PR #7274: Avoiding introducing dependency on the indices of a term whic...Pierre-Marie Pédrot
2018-07-26Merge PR #8150: Fix static declaration of plugins in coqpp.Emilio Jesus Gallego Arias
2018-07-25Remove object duplication for Constraint command.Gaëtan Gilbert
2018-07-25Hints use Declare to declare universes instead of a custom object.Gaëtan Gilbert
2018-07-25Merge PR #7859: Remove himsg.pr_puniverses, use @{} for universe printing in ...Pierre-Marie Pédrot
2018-07-25Fix #7900 previous commit fixes a bug when using side effects in obligations.Matthieu Sozeau
2018-07-25Merge PR #8133: Fixes #8126: issue with notations and nested applicationsEmilio Jesus Gallego Arias
2018-07-25Merge PR #734: [travis] Also run coqchk on HoTTEmilio Jesus Gallego Arias
2018-07-25In "redundant clause" pattern-matching error, show also the pattern (#7777).Hugo Herbelin
2018-07-25[sphinx] Add a way of skipping names in the indexes.Théo Zimmermann
2018-07-25kernel: missing check that all universes are declared.Matthieu Sozeau
2018-07-25Optimized dependencies for pattern-matching on only trivial patterns.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 22:15:35 +0000