| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-09-06 | changed statements of Rpower_lt and Rle_power and added | Yves Bertot | |
| Rlt_Rpower_l and pow_INR. Unfortunately theorems Rpower_lt and Rle_power are named inconsistently, in spite of their similarity. | |||
| 2017-09-06 | Merge PR #1022: Appveyor package | Maxime Dénès | |
| 2017-09-05 | read flags from project file for Compile Buffer | Paul Steckler | |
| 2017-09-05 | Refine does not evar-normalizes the goal preemptively. | Pierre-Marie Pédrot | |
| 2017-09-05 | Make AppVeyor generate Windows package. | Maxime Dénès | |
| 2017-09-05 | Binding the firstorder tactic. | Pierre-Marie Pédrot | |
| 2017-09-05 | Remove -debug option from Windows build script. | Maxime Dénès | |
| It is no longer accepted by Coq's ./configure. | |||
| 2017-09-05 | Get sources of cygwin packages after building the installer. | Maxime Dénès | |
| 2017-09-05 | Adapt Windows build script to new CoqIDE data installation directory. | Maxime Dénès | |
| 2017-09-05 | Print more of the Coq build output. | Maxime Dénès | |
| 2017-09-05 | Print Coq build output. | Maxime Dénès | |
| 2017-09-05 | In regression test mode, run cygwin setup to install dependencies. | Maxime Dénès | |
| 2017-09-05 | Export Ltac2.Notations in the Ltac2 entry module. | Pierre-Marie Pédrot | |
| 2017-09-05 | The absurd tactic now parses a constr. | Pierre-Marie Pédrot | |
| 2017-09-05 | Binding move and intro. | Pierre-Marie Pédrot | |
| 2017-09-05 | Merge PR #1011: fix test-suite/coq-makefile/findlib-package on windows after ↵ | Maxime Dénès | |
| #958 | |||
| 2017-09-05 | Introducing quotations for move locations. | Pierre-Marie Pédrot | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |