Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | * | Revert "Merge PR #873: New strategy based on open scopes for deciding which ↵ | 2018-03-09 | ||
| | | | | | | | | | | | | | | | | | | | | | notation to use among several of them" This reverts commit 9cac9db6446b31294d2413d920db0eaa6dd5d8a6, reversing changes made to 2f679ec5235257c9fd106c26c15049e04523a307. | |||
* | | | Merge PR #6923: Export options | 2018-03-09 | ||
|\ \ \ | |_|/ |/| | | ||||
| | * | Documentation for Cumulativity Weak Constraints. | 2018-03-09 | ||
| | | | ||||
* | | | Merge PR #6480: Allow Prop as source for coercions | 2018-03-09 | ||
|\ \ \ | |_|/ |/| | | ||||
* | | | Merge PR #6820: Tacticals assert_fails and assert_succeeds | 2018-03-09 | ||
|\ \ \ | ||||
| | | * | Documenting the Export modifier for options in CHANGES. | 2018-03-09 | ||
| |_|/ |/| | | ||||
| | * | doc and changes for coercion from prop/type | 2018-03-09 | ||
| |/ |/| | ||||
* | | Merge PR #6851: Fix #6830: coqdep VDFILE uses too many arguments for ↵ | 2018-03-09 | ||
|\ \ | | | | | | | | | | fiat-crypto/OSX | |||
* \ \ | Merge PR #6926: An experimental 'Show Extraction' command (grant feature ↵ | 2018-03-08 | ||
|\ \ \ | | | | | | | | | | | | | wish #4129) | |||
* \ \ \ | Merge PR #6743: Add notation {x & P} for sigT | 2018-03-08 | ||
|\ \ \ \ | ||||
* \ \ \ \ | Merge PR #6909: Deprecate Focus and Unfocus | 2018-03-08 | ||
|\ \ \ \ \ | ||||
* \ \ \ \ \ | Merge PR #6582: Mangle auto-generated names | 2018-03-08 | ||
|\ \ \ \ \ \ | ||||
* | | | | | | | [vernac] Warn when using “Require” in a section | 2018-03-07 | ||
| | | | | | | | ||||
* | | | | | | | Merge PR #6744: Add String.concat | 2018-03-07 | ||
|\ \ \ \ \ \ \ | ||||
| | | | | | * | | Add CHANGES and man entry for coqdep learning _CoqProject. | 2018-03-06 | ||
| | | | | | | | | ||||
| | | | | * | | | An experimental 'Show Extraction' command (grant feature wish #4129) | 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} | 2018-03-05 | ||
| | | | | | | | ||||
| | | * | | | | Deprecate Focus and Unfocus. | 2018-03-05 | ||
| | | | |/ / | | | |/| | | ||||
* | | | | | | Merge PR #6791: Removing compatibility support for versions older than 8.5. | 2018-03-04 | ||
|\ \ \ \ \ \ | ||||
| * | | | | | | CHANGES entry for #6791. | 2018-03-02 | ||
| | |_|/ / / | |/| | | | | ||||
* / | | | | | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-". | 2018-03-01 | ||
|/ / / / / | | | | | | | | | | | | | | | | Noticed by Sigurd Schneider. | |||
| | | | * | Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross). | 2018-02-28 | ||
| | | | | | ||||
| * | | | | Add String.concat | 2018-02-24 | ||
|/ / / / | ||||
* | | | | Merge PR #6599: Decimals in prelude | 2018-02-24 | ||
|\ \ \ \ | |_|_|/ |/| | | | ||||
* | | | | Merge PR #6604: Extend `zify_N` with knowledge about `N.pred` | 2018-02-21 | ||
|\ \ \ \ | ||||
| | * | | | Add CHANGES entry for decimals in prelude | 2018-02-20 | ||
| | | | | | ||||
* | | | | | Notations: Adding modifiers to tell which kind of binder a constr can parse. | 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. | 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. | 2018-02-20 | ||
| | | | | | ||||
* | | | | | Adding support for parsing subterms of a notation as "pattern". | 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 | 2018-02-17 | ||
| |/ / |/| | | ||||
| * | | Extend `zify_N` with knowledge about `N.pred` | 2018-02-14 | ||
| | | | | | | | | | | | | | | | by doing the same thing as `zify_nat` does for `nat.pred`. This fixes #6602. | |||
* | | | CHANGES for 8.7.2. | 2018-02-14 | ||
|/ / | ||||
* | | Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation) | 2018-02-14 | ||
|\ \ | ||||
| * | | Add CHANGES entry for #1047 | 2018-02-13 | ||
| | | | ||||
| | * | Add notation {x & P} for sigT | 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 | 2018-02-12 | ||
|/ | ||||
* | Merge PR #6629: Archive COMPATIBILITY | 2018-01-23 | ||
|\ | ||||
| * | Move the mention of the removal of Qed exporting at the right place. | 2018-01-22 | ||
| | | ||||
* | | Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction. | 2018-01-22 | ||
|\ \ | ||||
* | | | add flash infos about wrap, not found, no. of replacements, no. of finds, ↵ | 2018-01-18 | ||
| |/ |/| | | | | | issue #6452 | |||
* | | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder. | 2018-01-18 | ||
|\ \ | ||||
| | * | Add CHANGES entry | 2018-01-17 | ||
| | | | ||||
| * | | Add CHANGES entry | 2018-01-17 | ||
| |/ | ||||
* | | Merge PR #6551: Bracket with goal selector | 2018-01-16 | ||
|\ \ | |/ |/| | ||||
| * | Documentation and CHANGES for bracket with goal selector. | 2018-01-05 | ||
| | | ||||
* | | add optimize_heap tactic for #6488 | 2018-01-03 | ||
|/ | ||||
* | Merge PR #6377: Removal of the FAQ LaTex document. | 2017-12-20 | ||
|\ | ||||
* \ | Merge PR #6381: A version of [time] that works on constr evaluation | 2017-12-18 | ||
|\ \ | ||||
* \ \ | Merge PR #6380: Add tactics to reset and display the Ltac profile | 2017-12-18 | ||
|\ \ \ |