aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-06-26[declare] Fine tuning of Hook type.Emilio Jesus Gallego Arias
2019-06-26Merge PR #10401: Fix printers testEmilio Jesus Gallego Arias
2019-06-26Merge PR #10427: Move internal flagEmilio Jesus Gallego Arias
2019-06-25Re-add the "Show Goal" command for Prooftree in PG.Jim Fehrle
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 21:13:08 +0000