aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-10-31changelog for #10985Gaëtan Gilbert
2019-10-31Fix output testsGaëtan Gilbert
2019-10-31ppvernac: bidi hints use & not |Gaëtan Gilbert
2019-10-31Print argument info as an Arguments command in AboutGaëtan Gilbert
2019-10-31Move prettyp (Print implementation) to vernac/Gaëtan Gilbert
2019-10-31Doc: index command Arguments with assertGaëtan Gilbert
2019-10-31Move Arguments implementation to its own file (from vernacentries)Gaëtan Gilbert
2019-10-31Merge PR #10861: Fix #10615: Notation substitution for Ltac2 terms.Gaëtan Gilbert
2019-10-31[classes] Remove a couple of unneeded option typesEmilio Jesus Gallego Arias
2019-10-31[classes] Untabify in preparation for next commit.Emilio Jesus Gallego Arias
2019-10-31[classes] Some refactoring on proof save preparation.Emilio Jesus Gallego Arias
2019-10-31Fix #8459: anomaly not enough abstractions in fix bodyGaëtan Gilbert
2019-10-31Merge PR #11009: Rename the 2 local type_cstr nonterminals to give them uniqu...Pierre-Marie Pédrot
2019-10-31Merge PR #10995: add test for #4502 (fixed by unknown commit)Pierre-Marie Pédrot
2019-10-31Merge PR #10933: Add clarification in make-changelog.Gaëtan Gilbert
2019-10-31[Nix] Update reference to nixpkgsVincent Laporte
2019-10-30Merge PR #10953: [declare] Remove declare_scheme hook in DeclarePierre-Marie Pédrot
2019-10-30Merge PR #11004: [test-suite] Test section-local mutual Fixpoint.Pierre-Marie Pédrot
2019-10-30Rename the 2 local type_cstr nonterminals to give them unique namesJim Fehrle
2019-10-30Merge PR #10999: [refman] Give an example of contradiction when positivity ch...Clément Pit-Claudel
2019-10-30[test-suite] Test section-local mutual Fixpoint.Emilio Jesus Gallego Arias
2019-10-30Implement the unsupported attribute error using the warning systemGaëtan Gilbert
2019-10-30Use bullets and indentation (but the result rendering is weird).Théo Zimmermann
2019-10-30Use explicit match as suggested by Clément.Théo Zimmermann
2019-10-30[refman] Add a second example of contradiction when positivity checking is di...Théo Zimmermann
2019-10-30Make changelog script aware of trailing slashes.Arthur Azevedo de Amorim
2019-10-30make: guard cp calls with rm -f on executablesGaëtan Gilbert
2019-10-30[refman] Give an example of contradiction when positivity checking is disabled.Théo Zimmermann
2019-10-30[declare] Remove declare_scheme hook in DeclareEmilio Jesus Gallego Arias
2019-10-30Merge PR #10960: Move inference_hook from vernacentries to lemmasEmilio Jesus Gallego Arias
2019-10-30Merge PR #10973: Remove dead code in save_remaining_recthmsEmilio Jesus Gallego Arias
2019-10-30Merge PR #10981: [abstract] Remove un-unused reference to `evar_map`Pierre-Marie Pédrot
2019-10-30Merge PR #10303: Raise an anomaly when looking up unknown constant/inductivePierre-Marie Pédrot
2019-10-30Merge PR #10949: [declare] Provide helper for private constant inlining.Pierre-Marie Pédrot
2019-10-30Merge PR #10681: [declare] Make `proof_entry` a private type.Pierre-Marie Pédrot
2019-10-30Move start_proof_com from lemmas to vernacentriesGaëtan Gilbert
2019-10-30add test for #4502 (fixed by unknown commit)Gaëtan Gilbert
2019-10-30Merge PR #10494: Show diffs in "Show Proof."Enrico Tassi
2019-10-30Numbers.Cyclic: use “lia” rather than “omega”Vincent Laporte
2019-10-29Merge PR #10966: `assert_succeeds`&`assert_fails`: multisuccess fixGaëtan Gilbert
2019-10-29Show diffs in "Show Proof."Jim Fehrle
2019-10-29Use a less kludgy way of solving #9114Jason Gross
2019-10-29Fix #9114, assert_succeeds (exact I) solves goalJason Gross
2019-10-29`assert_succeeds`&`assert_fails`: multisuccess fixJason Gross
2019-10-29[abstract] Remove un-unused reference to `evar_map`Emilio Jesus Gallego Arias
2019-10-29[declare] Use helper function for `fix_exn` instead of relying on internals.Emilio Jesus Gallego Arias
2019-10-29[declare] Make `proof_entry` a private type.Emilio Jesus Gallego Arias
2019-10-29Merge PR #10892: [engine] Remove UnivGen.global_of_constrPierre-Marie Pédrot
2019-10-29Document the ability to bind notation arguments in Ltac2.Pierre-Marie Pédrot
2019-10-29Fix #10615: Notation substitution for Ltac2 terms.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 12:34:25 +0000