Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge PR#594: An example showing the benefit of Econstr | Maxime Dénès | 2017-05-11 |
|\ | |||
* \ | Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 a... | Maxime Dénès | 2017-05-11 |
|\ \ | |||
* \ \ | Merge PR#201: Transparent abstract | Maxime Dénès | 2017-05-11 |
|\ \ \ | |||
* \ \ \ | Merge PR#558: Adding a fold_glob_constr_with_binders combinator | Maxime Dénès | 2017-05-05 |
|\ \ \ \ | |||
| | | | * | Adding a test-suite pattern-unification example that Econstr fixed. | Hugo Herbelin | 2017-05-05 |
| |_|_|/ |/| | | | |||
* | | | | Merge PR#544: Anonymous universes | Maxime Dénès | 2017-05-05 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR#541: Fixing "decide equality" bug #5449 | Maxime Dénès | 2017-05-03 |
|\ \ \ \ \ | |||
| | * | | | | Type@{_} should not produce a flexible algebraic universe. | Gaetan Gilbert | 2017-05-03 |
| | * | | | | Allow flexible anonymous universes in instances and sorts. | Gaetan Gilbert | 2017-05-03 |
* | | | | | | Merge PR#411: Mention template polymorphism in the documentation. | Maxime Dénès | 2017-05-03 |
|\ \ \ \ \ \ | |_|/ / / / |/| | | | | | |||
* | | | | | | Fix bug #5501: Universe polymorphism breaks proof involving auto. | Pierre-Marie Pédrot | 2017-04-30 |
| | * | | | | Fixing "decide equality"'s bug #5449. | Hugo Herbelin | 2017-04-30 |
| |/ / / / |/| | | | | |||
* | | | | | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l... | Maxime Dénès | 2017-04-28 |
|\ \ \ \ \ | |||
| | | | | * | Test surgical use of beta-iota in the type of variables coming from | Hugo Herbelin | 2017-04-27 |
| |_|_|_|/ |/| | | | | |||
* | | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-04-27 |
|\ \ \ \ \ | |||
| | | | | * | Add transparent_abstract tactic | Jason Gross | 2017-04-25 |
| |_|_|_|/ |/| | | | | |||
* | | | | | Merge PR#574: Fix bug #5476: Ltac has an inconsistent view of hypotheses. | Maxime Dénès | 2017-04-24 |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR#565: Remove VernacError | Maxime Dénès | 2017-04-24 |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge branch v8.6 into trunk | Hugo Herbelin | 2017-04-22 |
|\ \ \ \ \ \ \ | |||
| | * | | | | | | Remove VernacError | Gaetan Gilbert | 2017-04-21 |
| |/ / / / / / |/| | | | | | | |||
| | | * | | | | Fix bug #5377: @? patterns broken. | Pierre-Marie Pédrot | 2017-04-20 |
| | |/ / / / | |/| | | | | |||
| | * | | | | Fix bug #5476: Ltac has an inconsistent view of hypotheses. | Pierre-Marie Pédrot | 2017-04-19 |
| |/ / / / |/| | | | | |||
| * | | | | Merge PR#538: Correction of bug #4306 | Maxime Dénès | 2017-04-19 |
| |\ \ \ \ | |||
* | | | | | | Add a test for bug #5321: clearbody breaks typing of goal. | Pierre-Marie Pédrot | 2017-04-17 |
* | | | | | | Merge branch 'v8.6' into trunk | Maxime Dénès | 2017-04-15 |
|\| | | | | | |||
| * | | | | | Fixing bug #5470 (anomaly on notations with misused "binder" type). | Hugo Herbelin | 2017-04-14 |
| * | | | | | Fixing bug #5469 (notation format not recognizing curly braces). | Hugo Herbelin | 2017-04-14 |
| * | | | | | Fix anomaly when doing [all:Check _.] during a proof. | Gaetan Gilbert | 2017-04-14 |
| | | | | * | Using fold_glob_constr_with_binders to code bound_glob_vars. | Hugo Herbelin | 2017-04-13 |
| | | | | * | Adding a fold_glob_constr_with_binders combinator. | Hugo Herbelin | 2017-04-13 |
* | | | | | | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r... | Maxime Dénès | 2017-04-12 |
|\ \ \ \ \ \ | |_|_|_|_|/ |/| | | | | | |||
| | | | | * | Update various comments to use "template polymorphism" | Gaetan Gilbert | 2017-04-11 |
| |_|_|_|/ |/| | | | | |||
* | | | | | Merge PR#532: Clean Nsatz implementation. | Maxime Dénès | 2017-04-11 |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR#537: Efficient side-effect abstraction | Maxime Dénès | 2017-04-11 |
|\ \ \ \ \ \ | |||
* | | | | | | | Adding a test for 'rewrite in *' when an evar is solved by side-effect. | Pierre-Marie Pédrot | 2017-04-10 |
* | | | | | | | Adding a test for the correctness of normalization in legacy typeclasses. | Pierre-Marie Pédrot | 2017-04-10 |
| | * | | | | | Fix an algorithmic issue in Nsatz. | Pierre-Marie Pédrot | 2017-04-09 |
| | | | | | * | Fixing several wrong computations of implicit arguments by position | Hugo Herbelin | 2017-04-09 |
| | | |_|_|/ | | |/| | | | |||
| | | | * | | Fixing #5460 (limitation in computing deps in pattern-matching compilation). | Hugo Herbelin | 2017-04-08 |
* | | | | | | Merge branch 'master' into econstr | Pierre-Marie Pédrot | 2017-04-07 |
|\ \ \ \ \ \ | | |/ / / / | |/| | | | | |||
| * | | | | | Merge PR#530: [toplevel] Remove exception error printer in favor of feedback ... | Maxime Dénès | 2017-04-07 |
| |\ \ \ \ \ | |||
| * \ \ \ \ \ | Merge PR#455: Farewell decl_mode | Maxime Dénès | 2017-04-06 |
| |\ \ \ \ \ \ | |||
| | | | | | * \ | Merge branch 'origin/v8.5' into v8.6. | Hugo Herbelin | 2017-04-06 |
| | | | | | |\ \ | |||
| | | * | | | | | | [toplevel] Remove exception error printer in favor of feedback printer. | Emilio Jesus Gallego Arias | 2017-04-05 |
| | |/ / / / / / | |/| | | | | | | |||
| | | | | | | * | closing bug file for #4306 | Julien Forest | 2017-04-04 |
| | | | | | | * | bug file for 4306 | Julien Forest | 2017-04-04 |
| | | * | | | | | Adding tests for chained abstract tactics. | Pierre-Marie Pédrot | 2017-04-04 |
| | |/ / / / / | |/| | | | | | |||
* | | | | | | | Merge branch 'trunk' into pr379 | Maxime Dénès | 2017-04-04 |
|\| | | | | | | |||
| | | | * | | | Test file for #5435: [Eval native_compute in] raises anomaly. | Maxime Dénès | 2017-04-04 |
| | | | | |/ | | | | |/| | |||
| * | | | | | Merge branch 'v8.6' into trunk | Maxime Dénès | 2017-04-03 |
| |\ \ \ \ \ | | | |_|/ / | | |/| | | |