aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-06-28Reify libobject containersMaxime Dénès
2019-06-27Merge PR #10443: Fix dev/doc/README.md by removing redundant, outdated info.Clément Pit-Claudel
2019-06-27Fix dev/doc/README.md by removing redundant, outdated info.Théo Zimmermann
2019-06-27Merge PR #10429: Perform the opaque section variable inference outside of the...Gaëtan Gilbert
2019-06-27Merge PR #10337: [stm] [vernac] Remove special ?proof parameter from vernac m...Enrico Tassi
2019-06-26[ci] Overlays for #10337Emilio Jesus Gallego Arias
2019-06-26[proof] finalize_proof doesn't need opaque (it's already in entries)Gaëtan Gilbert
2019-06-26Perform the opaque section variable inference outside of the kernel.Pierre-Marie Pédrot
2019-06-26Remove dead code for typing of section definitions in kernel.Pierre-Marie Pédrot
2019-06-26[stm] [vernac] Remove special ?proof parameter from vernac main pathEmilio Jesus Gallego Arias
2019-06-26Merge PR #9855: [Fail] Simplify `Fail` implementation.Gaëtan Gilbert
2019-06-26Merge PR #10351: [lemmas] Move `Stack` out of Lemmas.Gaëtan Gilbert
2019-06-26Merge PR #10401: Fix printers testEmilio Jesus Gallego Arias
2019-06-26Merge PR #10427: Move internal flagEmilio Jesus Gallego Arias
2019-06-25Merge PR #10344: Allow to pass Ltac2 values to Ltac1 quotationsEnrico Tassi
2019-06-25[lemmas] Move `Stack` out of Lemmas.Emilio Jesus Gallego Arias
2019-06-25Move the internal_flag type from Declare to Ind_tables.Pierre-Marie Pédrot
2019-06-25Remove the internal_flag argument from Declare API.Pierre-Marie Pédrot
2019-06-25Make dependence in Declare explicit in tactics.Pierre-Marie Pédrot
2019-06-25Give a functional type to Ltac1 quotations with a context.Pierre-Marie Pédrot
2019-06-25Documenting the Ltac2 change.Pierre-Marie Pédrot
2019-06-25Adding the ability to transfer Ltac2 variables to Ltac1 quotations.Pierre-Marie Pédrot
2019-06-25Merge PR #10316: [lemmas] Reify info for implicits, universe decls, and rec t...Pierre-Marie Pédrot
2019-06-25Merge PR #10219: [Ltac2] Add util files for Bool, List, OptionPierre-Marie Pédrot
2019-06-25Merge PR #10162: Fix #10161: occur check when defining an algebraic universe.Pierre-Marie Pédrot
2019-06-25Merge PR #10284: Expose set interface to option tablesPierre-Marie Pédrot
2019-06-25Merge PR #10412: Add output-coqtop test directory that runs output tests with...Enrico Tassi
2019-06-25Merge PR #10408: Fix coqdoc title: should be on a single line.Vincent Laporte
2019-06-24[proof] Remove last case of optional `?poly` arguments.Emilio Jesus Gallego Arias
2019-06-24Use named records instead of tuples where `polymorphic` used to be.Gaëtan Gilbert
2019-06-24[proof] dev/doc/changes for the last refactoringsEmilio Jesus Gallego Arias
2019-06-24[proof] Move initial_euctx to proof_globalEmilio Jesus Gallego Arias
2019-06-24[ci] Overlays for #10316Emilio Jesus Gallego Arias
2019-06-24[proof] API Documentation fixes.Emilio Jesus Gallego Arias
2019-06-24[api] [proof] Move `discharge` type to vernac_ast where it is used.Emilio Jesus Gallego Arias
2019-06-24[api] Remove `polymorphic` type alias, use labels instead.Emilio Jesus Gallego Arias
2019-06-24[api] Move `locality` from `library` to `vernac`.Emilio Jesus Gallego Arias
2019-06-24[lemmas] [proof] Split proof kinds into per-layer components.Emilio Jesus Gallego Arias
2019-06-24[proof] More uniformity in proof start labels.Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-27 04:06:06 +0000