aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-06-24[proof] Remove duplicated universe polymorphic from decl_kindsEmilio Jesus Gallego Arias
2019-06-24[proof] Remove redundant universe declaration information.Emilio Jesus Gallego Arias
2019-06-24[lemmas] Untabify.Emilio Jesus Gallego Arias
2019-06-24[lemmas] Turn Lemmas.info into a proper type with constructor.Emilio Jesus Gallego Arias
2019-06-24[fixpoint] Remove code duplication in (co) fixpoint declaration.Emilio Jesus Gallego Arias
2019-06-24[lemmas] Reify proof information for recursive theorems.Emilio Jesus Gallego Arias
2019-06-24[lemmas] Reify info for implicits, univ_decls, prepare for rec_thms.Emilio Jesus Gallego Arias
2019-06-24Merge PR #10428: Remove the export_seff flag from Declare API.Emilio Jesus Gallego Arias
2019-06-24Remove the export_seff flag from Declare API.Pierre-Marie Pédrot
2019-06-24Merge PR #10406: Desynchronize the type of proof and kernel entriesEmilio Jesus Gallego Arias
2019-06-24[test-suite] Fix printers testGaëtan Gilbert
2019-06-24Add overlays.Pierre-Marie Pédrot
2019-06-24Code simplification for definition_entry type.Pierre-Marie Pédrot
2019-06-24Remove the unused opaque_entry_inline_code field from opaque entries.Pierre-Marie Pédrot
2019-06-24Enforce that opaque entries carry their type.Pierre-Marie Pédrot
2019-06-24Dedicated type for opaque entries in the kernel.Pierre-Marie Pédrot
2019-06-24Enforce that transparent entries are forced beforehand.Pierre-Marie Pédrot
2019-06-24Take advantage of the change of entry representation to split opacity status.Pierre-Marie Pédrot
2019-06-24Duplicate the type of constant entries in Proof_global.Pierre-Marie Pédrot
2019-06-24Move Declare to tactics folder.Pierre-Marie Pédrot
2019-06-24Merge PR #10375: [lexer] correctly update line number when lexing QUOTATION (...Pierre-Marie Pédrot
2019-06-24Merge PR #10394: [ide] chop sentences taking into account QUOTATION tokenPierre-Marie Pédrot
2019-06-21Merge PR #10416: Elpi 1.4.0Emilio Jesus Gallego Arias
2019-06-21Merge PR #9665: [dune] Enable optimization options in the compilation of the VM.Théo Zimmermann
2019-06-21[ci] overlay for coq-elpiEnrico Tassi
2019-06-21[docker] [ci] Update Elpi to version 1.4.0Enrico Tassi
2019-06-21[dune] Enable optimization options in the compilation of the VM.Emilio Jesus Gallego Arias
2019-06-21Merge PR #10414: Add Conda badge to README.mdThéo Zimmermann
2019-06-21Add Conda badge to README.mdSamuel Lelièvre
2019-06-20Add output-coqtop test directory that runs output tests with coqtopJim Fehrle
2019-06-20Merge PR #9645: [proof] Remove terminator type, unifying regular and obligati...Pierre-Marie Pédrot
2019-06-20Fix coqdoc title: should be on a single line.Théo Zimmermann
2019-06-19[Fail] Tweaks to implementation.Emilio Jesus Gallego Arias
2019-06-19[Fail] Simplify `Fail` implementation.Emilio Jesus Gallego Arias
2019-06-19Merge PR #10380: [errors] remove "is_handled" logic, turn unhandled into anom...Gaëtan Gilbert
2019-06-19[test] unit tests for ide/coq_lex.mlEnrico Tassi
2019-06-19Removed backtracking and default variants of various functions and added opti...Michael Soegtrop
2019-06-19[test-suite] support for unit-tests/ide/ tests linking coq.ideEnrico Tassi
2019-06-19[META] fix dependencies of coq.ideEnrico Tassi
2019-06-19[ide] chop sentences taking into account QUOTATION tokenEnrico Tassi
2019-06-19Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations i...Théo Zimmermann
2019-06-18Merge PR #10398: Revert "Fix bug #5710"Pierre-Marie Pédrot
2019-06-18Removed "b" from function names in Bool.vMichael Soegtrop
2019-06-18[errors] remove "is_handled" logic, turn unhandled into anomaliesEmilio Jesus Gallego Arias
2019-06-18Revert "Fix bug #5710"Vincent Laporte
2019-06-18[lexer] correctly update line number when lexing QUOTATION (fix #10350)Enrico Tassi
2019-06-18Merge PR #9977: [dune] Support for coqide as an ocamldebug target.Gaëtan Gilbert
2019-06-18Merge PR #10199: Fix computation of implicit arguments when names collide in ...Maxime Dénès
2019-06-17Merge PR #10392: Fix the changelog of 8.10+beta2 following the backport of #1...Clément Pit-Claudel
2019-06-17Merge PR #10362: Kernel-side delaying of polymorphic opaque constantsGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 10:10:29 +0000