aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-08-12Merge PR #963: fix coq_makefileMaxime Dénès
2017-08-12Add some things Jason mentionedTej Chajed
2017-08-12Expand PR process explanationTej Chajed
2017-08-12Link to the existing list of tutorialsTej Chajed
2017-08-12fix coq_makefileMatej Košík
2017-08-12More portable location for the time command.Théo Zimmermann
2017-08-11Introducing a syntax for goal dispatch.Pierre-Marie Pédrot
2017-08-10Simplify a bit of wordingTej Chajed
2017-08-10Describe pull requests a bit more preciselyTej Chajed
2017-08-10Some more tweaks to contributing guideTej Chajed
2017-08-10Amendments to contributing docTej Chajed
2017-08-10Add a set of contributing guidelinesTej Chajed
2017-08-08Another batch of primitive operations.Pierre-Marie Pédrot
2017-08-08Set detachable windows type hint to dialog.Olivier Marty
2017-08-08Code simplification in quotations.Pierre-Marie Pédrot
2017-08-07Defining several aliases for built-in tactics.Pierre-Marie Pédrot
2017-08-07Defining abbreviations for tactics that can parse as atoms.Pierre-Marie Pédrot
2017-08-07Fix location of not-unit warning.Pierre-Marie Pédrot
2017-08-07Fix parsing of parenthesized expressions.Pierre-Marie Pédrot
2017-08-07Defining a few base tacticals.Pierre-Marie Pédrot
2017-08-07Introducing grammar-free tactic notations.Pierre-Marie Pédrot
2017-08-07Add build_coq_or to APISigurd Schneider
2017-08-06Print names of all open blocksTej Chajed
2017-08-05Exporting more reduction functions.Pierre-Marie Pédrot
2017-08-05More notations for basic tactics.Pierre-Marie Pédrot
2017-08-05Exporting the rewrite tactic.Pierre-Marie Pédrot
2017-08-04Introducing quotations for the rewrite tactic.Pierre-Marie Pédrot
2017-08-04Makefile: install-byte works even if -coqide noEnrico Tassi
2017-08-04Adding locations to quotation types.Pierre-Marie Pédrot
2017-08-04More precise type for quoted structures.Pierre-Marie Pédrot
2017-08-04Adding the induction and destruct tactics.Pierre-Marie Pédrot
2017-08-04Introducing notations for destruct and induction arguments.Pierre-Marie Pédrot
2017-08-03Amend wording to capture intended meaningSam Pablo Kuper
2017-08-02Inserting enter functions in Ltac1 bindings.Pierre-Marie Pédrot
2017-08-02Tentatively implementing apply.Pierre-Marie Pédrot
2017-08-02Typo in documentation.Pierre-Marie Pédrot
2017-08-02Expanding documentation.Pierre-Marie Pédrot
2017-08-02Fix compilation of horrible Ltac2 example.Pierre-Marie Pédrot
2017-08-02Properly implementing the notation to easily access hypotheses.Pierre-Marie Pédrot
2017-08-02Code factorization in elim notation.Pierre-Marie Pédrot
2017-08-02Merging the e/- variants of primitive tactics.Pierre-Marie Pédrot
2017-08-02Rewording the introductionEnrico Tassi
2017-08-02Rephrasing a couple of sentences in a more factual way.Hugo Herbelin
2017-08-02Rephrasing the introduction in a more factual and up-to-date way.Hugo Herbelin
2017-08-02Port ssr manual to Coq's latex/hevea styleEnrico Tassi
2017-08-02Makefile.doc: implement serve-refman-8080 targetEnrico Tassi
2017-08-02Adding new notations.Pierre-Marie Pédrot
2017-08-02Extending the set of tactic scopes.Pierre-Marie Pédrot
2017-08-02Update Setoid.texlarsr
2017-08-02More examplesPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-26 14:00:45 +0000