aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2017-08-02Makefile: 'make clean' now immune to the check for binary files without sourcesPierre Letouzey
2017-08-02Properly classifying Ltac2 notations.Pierre-Marie Pédrot
2017-08-02Fixing parsing of match branches.Pierre-Marie Pédrot
2017-08-02Removing deprecated stuff.Pierre-Marie Pédrot
2017-08-02Typo in the documentation of cumulativityAmin Timany
2017-08-02Adding a few standard notations for Ltac1 tactics.Pierre-Marie Pédrot
2017-08-02Bindings use open constr quotations.Pierre-Marie Pédrot
2017-08-02Adding the open_constr scopePierre-Marie Pédrot
2017-08-02Better test Makefile.Pierre-Marie Pédrot
2017-08-02Tentatively fixing a few parsing issues.Pierre-Marie Pédrot
2017-08-02Fixup reification of egeneralize.Pierre-Marie Pédrot
2017-08-01More primitive tactics.Pierre-Marie Pédrot
2017-08-01Expanding unification variables in typechecking error messages.Pierre-Marie Pédrot
2017-08-01Don't reuse Coq AST for binding quotations.Pierre-Marie Pédrot
2017-08-01Fix parsing of fresh ident antiquotations.Pierre-Marie Pédrot
2017-08-01Introducing the all-mighty intro-patterns.Pierre-Marie Pédrot
2017-08-01Unbreak RecTutorial.vGaëtan Gilbert
2017-08-01Remove old doc/rt files.Gaëtan Gilbert
2017-08-01Add dev/v8-syntax/check-grammar byproducts to gitignore.Gaëtan Gilbert
2017-08-01Remove obsolete filesGaëtan Gilbert
2017-08-01Add .v extension to dev/doc/notes-on-conversionGaëtan Gilbert
2017-08-01Remove dev/TODOGaëtan Gilbert
2017-08-01Fix syntax-v8.tex bad parenthesizingGaëtan Gilbert
2017-08-01Remove unused Makefiles in dev/tools/Gaëtan Gilbert
2017-08-01[flags] Remove XML output flag.Emilio Jesus Gallego Arias
2017-08-01Remove understand_tcc_evars.Maxime Dénès
2017-08-01Move type_uconstr to Tacinterp.Maxime Dénès
2017-08-01Have coq-dpdgraph ci test print the differencesJason Gross
2017-08-01Remove understand_judgment and understand_judgment_tcc.Maxime Dénès
2017-08-01Remove allow_anonymous_refs.Maxime Dénès
2017-08-01Remove pure_open_constr (now open_constr)Maxime Dénès
2017-08-01Fix documentation.Pierre-Marie Pédrot
2017-08-01Printing goals does not evar-normalizes beforehand anymore.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-01 00:28:01 +0000