Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | | 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 | |
|/ / / / | ||||
| * | | | Addressing OCaml compilation warnings. | Hugo Herbelin | 2016-09-16 | |
* | | | | Make the Coq codebase independent from Ltac-related code. | Pierre-Marie Pédrot | 2016-09-16 | |
|\ \ \ \ | ||||
| * | | | | Untangling Tacexpr from lower strata. | Pierre-Marie Pédrot | 2016-09-15 | |
| * | | | | Moving Ltac-specific generic arguments to their own file in the ltac/ folder. | Pierre-Marie Pédrot | 2016-09-15 | |
| * | | | | Generalizing the notion of constr substitution to generic arguments. | Pierre-Marie Pédrot | 2016-09-15 | |
* | | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-09-14 | |
|\ \ \ \ \ | |/ / / / |/| / / / | |/ / / | ||||
| * | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-09-14 | |
| |\| | | ||||
| | * | | Fixing a recursive notation bug raised on coq-club on Sep 12, 2016. | Hugo Herbelin | 2016-09-12 | |
* | | | | Merge PR #244. | Pierre-Marie Pédrot | 2016-09-08 | |
|\ \ \ \ | ||||
* \ \ \ \ | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-09-02 | |
|\ \ \ \ \ | | |/ / / | |/| | | | ||||
| * | | | | Notation_ops.subst_glob_vars: substituting also in evar kind for | Hugo Herbelin | 2016-09-01 |