aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-09-05Binding the inversion family of tactics.Pierre-Marie Pédrot
2017-09-05Merge PR #1020: .mailmap updateGuillaume Melquiond
2017-09-05Merge PR #1010: Move mention of native_compute profiling in CHANGESMaxime Dénès
2017-09-05Merge PR #1021: Fix Software Foundations build.Maxime Dénès
2017-09-05.mailmap updateGaëtan Gilbert
2017-09-05Fix Software Foundations build.Maxime Dénès
2017-09-05Update CREDITS on a best-effort basis.Théo Zimmermann
2017-09-05A few more notations.Pierre-Marie Pédrot
2017-09-05Typeclasses_eauto strategy is now optional.Pierre-Marie Pédrot
2017-09-05Fixup grammar of typeclasses_eauto.Pierre-Marie Pédrot
2017-09-05Quotations for auto-related tactics.Pierre-Marie Pédrot
2017-09-05More static invariants for typeclass_eauto.Pierre-Marie Pédrot
2017-09-05ML bindings of auto-related tactics.Pierre-Marie Pédrot
2017-09-04Notation for "clear - ids".Pierre-Marie Pédrot
2017-09-04More notations for primitive tactics.Pierre-Marie Pédrot
2017-09-04More precise error messages for scope failure.Pierre-Marie Pédrot
2017-09-04Implementing the non-strict mode.Pierre-Marie Pédrot
2017-09-04Better backtraces for a few datatypes.Pierre-Marie Pédrot
2017-09-04Quick-and-dirty backtrace mechanism for the interpreter.Pierre-Marie Pédrot
2017-09-04fix test-suite/coq-makefile/findlib-package on windowsEnrico Tassi
2017-09-04Merge PR #1018: Avoid reinstalling some Cygwin dependencies on AppVeyor.Maxime Dénès
2017-09-04Avoid reinstalling some Cygwin dependencies on AppVeyor.Maxime Dénès
2017-09-04Updated gitignore.Pierre-Marie Pédrot
2017-09-04Closures now wear the constant they originated from.Pierre-Marie Pédrot
2017-09-04Fix coq/ltac2#17: Assertion failed. on only shelved goals remaining.Pierre-Marie Pédrot
2017-09-04Implementing multi-match and simple match over constrs.Pierre-Marie Pédrot
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
2017-09-04Implementing lazy matching over terms.Pierre-Marie Pédrot
2017-09-04Proper anomalies for missing registered primitives.Pierre-Marie Pédrot
2017-09-03Introducing a macro for constr matching.Pierre-Marie Pédrot
2017-09-03Addressing BZ#5713 (classical_left/classical_right artificially restricted).Hugo Herbelin
2017-09-03Moving generic arguments to Tac2quote.Pierre-Marie Pédrot
2017-09-03Uniform handling of locations in the various AST.Pierre-Marie Pédrot
2017-09-03Allowing ML objects to return mere tactic expressions.Pierre-Marie Pédrot
2017-09-03Allowing complex types in ML objects.Pierre-Marie Pédrot
2017-09-032 Typos in 'Add Parametric Morphism' Documentationstaffehn
2017-09-03Fix coq/ltac2#16: Passing Ltac2 variables to Ltac1 via $ results in anomalies.Pierre-Marie Pédrot
2017-09-02Fix coq/ltac2#12: Error should name which match cases are unhandled.Pierre-Marie Pédrot
2017-09-02Fix coq/ltac2#15: Ltac2 scope cannot be disabled after it is required.Pierre-Marie Pédrot
2017-09-01add option index entry for NativeCompute ProfilingPaul Steckler
2017-09-01move mention of native_compute profiling in CHANGESPaul Steckler
2017-09-01Fixing various typos in the Credits chapter.Théo Zimmermann
2017-09-01Do not hashcons universes beforehand.Pierre-Marie Pédrot
2017-09-01Bump MacOS version number and magic numbers.Maxime Dénès
2017-09-01Change version string to 8.8+alpha.Maxime Dénès
2017-09-01Ensuring the Ltac definitions have lowercase names.Pierre-Marie Pédrot
2017-09-01Passing an optional message to Tactic_failure.Pierre-Marie Pédrot
2017-08-31Properly handling internal errors from Coq.Pierre-Marie Pédrot
2017-08-31Expand the primitive functions on terms.Pierre-Marie Pédrot
2017-08-31Fix coq/ltac2#10: Antiquotation syntax breaks when backtracking across `Requi...Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-26 05:36:06 +0000