Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #7103: Fix #7101: STM delegation policy broken | Enrico Tassi | 2018-04-09 |
|\ | | | | | | | | | # Conflicts: # CHANGES | ||
* | | Fix #6404 - Print tactics called by ML tactics | Jason Gross | 2018-04-02 |
| | | |||
* | | Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092) | Pierre-Marie Pédrot | 2018-04-01 |
|\ \ | |||
* | | | Add CHANGES for removing Implicit Arguments and Arguments Scope | Jasper Hugunin | 2018-03-30 |
| | | | |||
| * | | Supporting fix/cofix in Ltac pattern-matching (wish #7092). | Hugo Herbelin | 2018-03-28 |
|/ / | | | | | | | | | This is done by not failing for fix/cofix while translating from glob_constr to constr_pattern. | ||
| * | Fix #7101: STM delegation policy broken | Maxime Dénès | 2018-03-28 |
|/ | | | | | I make here a minimal fix, but a lot of cleaning should be done around Aux_file handling, including removing some code from the kernel. | ||
* | Merge PR #7018: Fix typo in CHANGES. | Maxime Dénès | 2018-03-23 |
|\ | |||
* | | update CHANGES | Enrico Tassi | 2018-03-23 |
| | | |||
| * | Fix typo in CHANGES. | Théo Zimmermann | 2018-03-19 |
|/ | | | | [skip ci] | ||
* | Add some missing entries in CHANGES | Maxime Dénès | 2018-03-15 |
| | |||
* | [doc] Document removal of deprecated options. | Emilio Jesus Gallego Arias | 2018-03-09 |
| | |||
* | Merge PR #6949: Revert PR #873: New strategy based on open scopes for ↵ | Maxime Dénès | 2018-03-09 |
|\ | | | | | | | deciding… | ||
* \ | Merge PR #6775: Allow using cumulativity without forcing strict constraints. | Maxime Dénès | 2018-03-09 |
|\ \ | |||
| | * | Revert "Merge PR #873: New strategy based on open scopes for deciding which ↵ | Maxime Dénès | 2018-03-09 |
| | | | | | | | | | | | | | | | | | | | | | notation to use among several of them" This reverts commit 9cac9db6446b31294d2413d920db0eaa6dd5d8a6, reversing changes made to 2f679ec5235257c9fd106c26c15049e04523a307. | ||
* | | | Merge PR #6923: Export options | Maxime Dénès | 2018-03-09 |
|\ \ \ | |_|/ |/| | | |||
| | * | Documentation for Cumulativity Weak Constraints. | Gaëtan Gilbert | 2018-03-09 |
| | | | |||
* | | | Merge PR #6480: Allow Prop as source for coercions | Maxime Dénès | 2018-03-09 |
|\ \ \ | |_|/ |/| | | |||
* | | | Merge PR #6820: Tacticals assert_fails and assert_succeeds | Maxime Dénès | 2018-03-09 |
|\ \ \ | |||
| | | * | Documenting the Export modifier for options in CHANGES. | Pierre-Marie Pédrot | 2018-03-09 |
| |_|/ |/| | | |||
| | * | doc and changes for coercion from prop/type | charguer | 2018-03-09 |
| |/ |/| | |||
* | | Merge PR #6851: Fix #6830: coqdep VDFILE uses too many arguments for ↵ | Maxime Dénès | 2018-03-09 |
|\ \ | | | | | | | | | | fiat-crypto/OSX | ||
* \ \ | Merge PR #6926: An experimental 'Show Extraction' command (grant feature ↵ | Maxime Dénès | 2018-03-08 |
|\ \ \ | | | | | | | | | | | | | wish #4129) | ||
* \ \ \ | Merge PR #6743: Add notation {x & P} for sigT | Maxime Dénès | 2018-03-08 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6909: Deprecate Focus and Unfocus | Maxime Dénès | 2018-03-08 |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6582: Mangle auto-generated names | Maxime Dénès | 2018-03-08 |
|\ \ \ \ \ \ | |||
* | | | | | | | [vernac] Warn when using “Require” in a section | Vincent Laporte | 2018-03-07 |
| | | | | | | | |||
* | | | | | | | Merge PR #6744: Add String.concat | Maxime Dénès | 2018-03-07 |
|\ \ \ \ \ \ \ | |||
| | | | | | * | | Add CHANGES and man entry for coqdep learning _CoqProject. | Gaëtan Gilbert | 2018-03-06 |
| | | | | | | | | |||
| | | | | * | | | An experimental 'Show Extraction' command (grant feature wish #4129) | Pierre Letouzey | 2018-03-06 |
| | | | | |/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Attempt to extract the current ongoing proof (request by Clément Pit-Claudel on coqdev, and also #4129). Evars are handled as axioms. | ||
* | | | | | | | CHANGES and tests for with Definition @{univs} | Gaëtan Gilbert | 2018-03-05 |
| | | | | | | | |||
| | | * | | | | Deprecate Focus and Unfocus. | Théo Zimmermann | 2018-03-05 |
| | | | |/ / | | | |/| | | |||
* | | | | | | Merge PR #6791: Removing compatibility support for versions older than 8.5. | Maxime Dénès | 2018-03-04 |
|\ \ \ \ \ \ | |||
| * | | | | | | CHANGES entry for #6791. | Théo Zimmermann | 2018-03-02 |
| | |_|/ / / | |/| | | | | |||
* / | | | | | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-". | Hugo Herbelin | 2018-03-01 |
|/ / / / / | | | | | | | | | | | | | | | | Noticed by Sigurd Schneider. | ||
| | | | * | Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross). | Hugo Herbelin | 2018-02-28 |
| | | | | | |||
| * | | | | Add String.concat | Jason Gross | 2018-02-24 |
|/ / / / | |||
* | | | | Merge PR #6599: Decimals in prelude | Maxime Dénès | 2018-02-24 |
|\ \ \ \ | |_|_|/ |/| | | | |||
* | | | | Merge PR #6604: Extend `zify_N` with knowledge about `N.pred` | Maxime Dénès | 2018-02-21 |
|\ \ \ \ | |||
| | * | | | Add CHANGES entry for decimals in prelude | Jason Gross | 2018-02-20 |
| | | | | | |||
* | | | | | Notations: Adding modifiers to tell which kind of binder a constr can parse. | Hugo Herbelin | 2018-02-20 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Concretely, we provide "constr as ident", "constr as strict pattern" and "constr as pattern". This tells to parse a binder as a constr, restricting to only ident or to only a strict pattern, or to a pattern which can also be an ident. The "strict pattern" modifier allows to restrict the use of patterns in printing rules. This allows e.g. to select the appropriate rule for printing between {x|P} and {'pat|P}. | ||
* | | | | | More flexibility in locating or referring to a notation. | Hugo Herbelin | 2018-02-20 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We generalize the possibility to refer to a notation not only by its "_ U _" form but also using its "a 'U' b". (Wish from EJGA) | ||
* | | | | | A first step at refreshing and documenting the new feature. | Hugo Herbelin | 2018-02-20 |
| | | | | | |||
* | | | | | Adding support for parsing subterms of a notation as "pattern". | Hugo Herbelin | 2018-02-20 |
| |/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows in particular to define notations with 'pat style binders. E.g.: A non-trivial change in this commit is storing binders and patterns separately from terms. This is not strictly necessary but has some advantages. However, it is relatively common to have binders also used as terms, or binders parsed as terms. Thus, it is already relatively common to embed binders into terms (see e.g. notation for ETA in output test Notations3.v) or to coerce terms to idents (see e.g. the notation for {x|P} where x is parsed as a constr). So, it is as simple to always store idents (and eventually patterns) as terms. | ||
| | * | | Implement name mangling option | Jasper Hugunin | 2018-02-17 |
| |/ / |/| | | |||
| * | | Extend `zify_N` with knowledge about `N.pred` | Joachim Breitner | 2018-02-14 |
| | | | | | | | | | | | | | | | by doing the same thing as `zify_nat` does for `nat.pred`. This fixes #6602. | ||
* | | | CHANGES for 8.7.2. | Théo Zimmermann | 2018-02-14 |
|/ / | |||
* | | Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation) | Maxime Dénès | 2018-02-14 |
|\ \ | |||
| * | | Add CHANGES entry for #1047 | Tej Chajed | 2018-02-13 |
| | | | |||
| | * | Add notation {x & P} for sigT | Tej Chajed | 2018-02-12 |
| |/ | | | | | | | | | Analogous to existing `{x | P}` notation for `sig`, where the type of `x` is inferred instead of specified. | ||
* / | CHANGES for universe variance | Gaëtan Gilbert | 2018-02-12 |
|/ |