| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-09-05 | Binding the inversion family of tactics. | Pierre-Marie Pédrot | |
| 2017-09-05 | Merge PR #1020: .mailmap update | Guillaume Melquiond | |
| 2017-09-05 | Merge PR #1010: Move mention of native_compute profiling in CHANGES | Maxime Dénès | |
| 2017-09-05 | Merge PR #1021: Fix Software Foundations build. | Maxime Dénès | |
| 2017-09-05 | .mailmap update | Gaëtan Gilbert | |
| 2017-09-05 | Fix Software Foundations build. | Maxime Dénès | |
| The Software Foundations archive has been replaced by three volumes. | |||
| 2017-09-05 | Update CREDITS on a best-effort basis. | Théo Zimmermann | |
| And with help from https://github.com/coq/coq/graphs/contributors | |||
| 2017-09-05 | A few more notations. | Pierre-Marie Pédrot | |
| 2017-09-05 | Typeclasses_eauto strategy is now optional. | Pierre-Marie Pédrot | |
| 2017-09-05 | Fixup grammar of typeclasses_eauto. | Pierre-Marie Pédrot | |
| 2017-09-05 | Quotations for auto-related tactics. | Pierre-Marie Pédrot | |
| 2017-09-05 | More static invariants for typeclass_eauto. | Pierre-Marie Pédrot | |
| 2017-09-05 | ML bindings of auto-related tactics. | Pierre-Marie Pédrot | |
| 2017-09-04 | Notation for "clear - ids". | Pierre-Marie Pédrot | |
| 2017-09-04 | More notations for primitive tactics. | Pierre-Marie Pédrot | |
| 2017-09-04 | More precise error messages for scope failure. | Pierre-Marie Pédrot | |
| 2017-09-04 | Implementing the non-strict mode. | Pierre-Marie Pédrot | |
| 2017-09-04 | Better backtraces for a few datatypes. | Pierre-Marie Pédrot | |
| 2017-09-04 | Quick-and-dirty backtrace mechanism for the interpreter. | Pierre-Marie Pédrot | |
| 2017-09-04 | fix test-suite/coq-makefile/findlib-package on windows | Enrico Tassi | |
| 2017-09-04 | Merge PR #1018: Avoid reinstalling some Cygwin dependencies on AppVeyor. | Maxime Dénès | |
| 2017-09-04 | Avoid reinstalling some Cygwin dependencies on AppVeyor. | Maxime Dénès | |
| For some reason, OPAM was not happy after we reinstalled curl. | |||
| 2017-09-04 | Updated gitignore. | Pierre-Marie Pédrot | |
| 2017-09-04 | Closures now wear the constant they originated from. | Pierre-Marie Pédrot | |
| 2017-09-04 | Fix coq/ltac2#17: Assertion failed. on only shelved goals remaining. | Pierre-Marie Pédrot | |
| We check that the goal tactic is focussed before calling enter_one. | |||
| 2017-09-04 | Implementing multi-match and simple match over constrs. | Pierre-Marie Pédrot | |
| 2017-09-04 | Making detyping potentially lazy. | Pierre-Marie Pédrot | |
| The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager. | |||
| 2017-09-04 | Implementing lazy matching over terms. | Pierre-Marie Pédrot | |
| 2017-09-04 | Proper anomalies for missing registered primitives. | Pierre-Marie Pédrot | |
| 2017-09-03 | Introducing a macro for constr matching. | Pierre-Marie Pédrot | |
| 2017-09-03 | Addressing BZ#5713 (classical_left/classical_right artificially restricted). | Hugo Herbelin | |
| As explained in BZ#5713 report, the requirement for a non-empty context is not needed, so we remove it. | |||
| 2017-09-03 | Moving generic arguments to Tac2quote. | Pierre-Marie Pédrot | |
| 2017-09-03 | Uniform handling of locations in the various AST. | Pierre-Marie Pédrot | |
| 2017-09-03 | Allowing ML objects to return mere tactic expressions. | Pierre-Marie Pédrot | |
| 2017-09-03 | Allowing complex types in ML objects. | Pierre-Marie Pédrot | |
| 2017-09-03 | 2 Typos in 'Add Parametric Morphism' Documentation | staffehn | |
| 2017-09-03 | Fix coq/ltac2#16: Passing Ltac2 variables to Ltac1 via $ results in anomalies. | Pierre-Marie Pédrot | |
| 2017-09-02 | Fix coq/ltac2#12: Error should name which match cases are unhandled. | Pierre-Marie Pédrot | |
| 2017-09-02 | Fix coq/ltac2#15: Ltac2 scope cannot be disabled after it is required. | Pierre-Marie Pédrot | |
| Instead of setting globally the option, we add a hook to set it in the init object of the plugin. | |||
| 2017-09-01 | add option index entry for NativeCompute Profiling | Paul Steckler | |
| 2017-09-01 | move mention of native_compute profiling in CHANGES | Paul Steckler | |
| 2017-09-01 | Fixing various typos in the Credits chapter. | Théo Zimmermann | |
| 2017-09-01 | Do not hashcons universes beforehand. | Pierre-Marie Pédrot | |
| This should save a lot of useless reallocations and hashset crawling, which end up costing a lot. | |||
| 2017-09-01 | Bump MacOS version number and magic numbers. | Maxime Dénès | |
| 2017-09-01 | Change version string to 8.8+alpha. | Maxime Dénès | |
| 2017-09-01 | Ensuring the Ltac definitions have lowercase names. | Pierre-Marie Pédrot | |
| 2017-09-01 | Passing an optional message to Tactic_failure. | Pierre-Marie Pédrot | |
| 2017-08-31 | Properly handling internal errors from Coq. | Pierre-Marie Pédrot | |
| 2017-08-31 | Expand the primitive functions on terms. | Pierre-Marie Pédrot | |
| 2017-08-31 | Fix coq/ltac2#10: Antiquotation syntax breaks when backtracking across ↵ | Pierre-Marie Pédrot | |
| `Require`. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |