Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge branch 'trunk' into pr379 | Maxime Dénès | 2017-03-24 |
|\ | |||
| * | [safe_string] interp/dumpglob | Emilio Jesus Gallego Arias | 2017-03-14 |
| * | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-02-22 |
| |\ | |||
| * \ | Merge PR#189: Remove tabulation support from pretty-printing. | Maxime Dénès | 2017-02-20 |
| |\ \ | |||
* | | | | Merge branch 'master'. | Pierre-Marie Pédrot | 2017-02-14 |
|\| | | | |||
* | | | | Namegen primitives now apply on evar constrs. | Pierre-Marie Pédrot | 2017-02-14 |
* | | | | Definining EConstr-based contexts. | Pierre-Marie Pédrot | 2017-02-14 |
* | | | | Removing various compatibility layers of tactics. | Pierre-Marie Pédrot | 2017-02-14 |
* | | | | Ltac now uses evar-based constrs. | Pierre-Marie Pédrot | 2017-02-14 |
* | | | | Reductionops now return EConstrs. | Pierre-Marie Pédrot | 2017-02-14 |
* | | | | Tactics API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | | | Pretyping API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | | | Classops API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | | | | Reductionops API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| | | * | Turning an anomaly on 'pat into a proper "unsupported" error message. | Hugo Herbelin | 2017-02-09 |
| | | * | Fixing an anomaly with 'pat after cofix. | Hugo Herbelin | 2017-02-02 |
| * | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-02-01 |
| |\ \ \ | | | |/ | | |/| | |||
| | * | | Fixing #5326 (anomaly on some unsupported case of 'pat). | Hugo Herbelin | 2017-01-26 |
| * | | | Adding a new evar source to remember the name of evars which were | Hugo Herbelin | 2017-01-22 |
|/ / / | |||
* | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-29 |
|\| | | |||
| * | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-29 |
| |\ \ | |||
| | * | | Fixing #5161 (case of a notation with unability to detect a recursive binder). | Hugo Herbelin | 2016-10-27 |
* | | | | CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript". | Matej Kosik | 2016-10-19 |
* | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-17 |
|\| | | | |||
| | * | | Merge PR #310 into v8.5 | Pierre-Marie Pédrot | 2016-10-17 |
| | |\ \ | |||
| * | \ \ | Merge PR #310 into v8.6 | Pierre-Marie Pédrot | 2016-10-17 |
| |\ \ \ \ | | | |/ / | | |/| | | |||
| * | | | | Merge PR #289 into v8.6. | Pierre-Marie Pédrot | 2016-10-12 |
| |\ \ \ \ | |||
* | | | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-12 |
|\| | | | | | |||
| | | | * | | Fixing a collision about the meta-variable ".." in recursive notations. | Hugo Herbelin | 2016-10-12 |
| * | | | | | Shorter message for "Test Asymmetric Patterns". | Hugo Herbelin | 2016-10-12 |
| * | | | | | Fixing a few confusions on the name of the beautify flag. | Hugo Herbelin | 2016-10-12 |
* | | | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-08 |
|\| | | | | | |||
| | | * | | | Revert "Make the pretty printer resilient to incomplete nametab (progress on ... | Théo Zimmermann | 2016-10-06 |
| | | |/ / | |||
| * | | | | Disable compatibility notations warnings. | Maxime Dénès | 2016-10-06 |
| * | | | | Remove the Set Verbose Compat option and turn the warning on by default. | Maxime Dénès | 2016-10-06 |
* | | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-05 |
|\| | | | | |||
| * | | | | Fix #5048 - Casts in pattern raise an anomaly in Constrintern. | Maxime Dénès | 2016-10-04 |
| * | | | | Quick fix to #4595 (making notations containing "ltac:" unused for printing). | Hugo Herbelin | 2016-10-04 |
* | | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-02 |
|\| | | | | |||
| * | | | | Fix bug #5087: Improve the error message on record with duplicated fields. | Pierre-Marie Pédrot | 2016-10-02 |
| * | | | | Warning about similar notations now up to alpha-conversion. | Hugo Herbelin | 2016-09-28 |
| | * | | | [notation] Allow to retrieve defined notations. | Emilio Jesus Gallego Arias | 2016-09-25 |
| |/ / / | |||
* | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-09-23 |
|\| | | | |||
| * | | | coqc -o now places .glob file near .vo file | Enrico Tassi | 2016-09-22 |
| * | | | typos | Enrico Tassi | 2016-09-22 |
* | | | | Revert "Merge remote-tracking branch 'github/pr/283' into trunk" | Maxime Dénès | 2016-09-22 |
* | | | | Merge remote-tracking branch 'github/pr/283' into trunk | Maxime Dénès | 2016-09-22 |
|\ \ \ \ | |||
* | | | | | Fix an error-prone error API. | Pierre-Marie Pédrot | 2016-09-21 |
* | | | | | Merging Stdarg and Constrarg. | Pierre-Marie Pédrot | 2016-09-21 |
| * | | | | Rename Decl_kinds.binding_kind into Decls_kind.implicit_status. | Maxime Dénès | 2016-09-20 |
|/ / / / |