aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2017-08-01Detyping functions are now operating on EConstr.t.Pierre-Marie Pédrot
2017-08-01Binding more primitive tactics.Pierre-Marie Pédrot
2017-08-01Fix typos. Improve wording.Sam Pablo Kuper
2017-08-01More in documentation.Pierre-Marie Pédrot
2017-08-01Improve style slightlySam Pablo Kuper
2017-08-01Move glob_constr_ltac_closure to evar_refiner.Maxime Dénès
2017-08-01Merge PR #933: Fix documentation of Hint Mode (bug #4911).Maxime Dénès
2017-08-01Merge PR #932: Fix shuffled documentation.Maxime Dénès
2017-08-01Merge PR #929: Add missing paragraph to introductionMaxime Dénès
2017-08-01Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).Maxime Dénès
2017-08-01Merge PR #926: test-suite uses Extraction TestCompileMaxime Dénès
2017-08-01Merge PR #925: Document Extraction TestCompileMaxime Dénès
2017-08-01Merge PR #921: [make] remove compat5 file.Maxime Dénès
2017-08-01Merge PR #919: Remove a few useless evar-normalizations in printing code.Maxime Dénès
2017-08-01Merge PR #917: Moving --print-version to -print-version for consistency.Maxime Dénès
2017-08-01Merge PR #913: Less allocations in DetypingMaxime Dénès
2017-08-01Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-26 15:10:54 +0000