aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs
Commit message (Expand)AuthorAge
...
* | | | | | Fix #6956: Uncaught exception in bytecode compilationGravatar Maxime Dénès2018-04-06
| |_|/ / / |/| | | |
| * | | | Fix #5981, bugs/opened/3263.v is non-deterministic by removing the test.Gravatar Théo Zimmermann2018-04-05
|/ / / /
* | | | Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)Gravatar Pierre-Marie Pédrot2018-04-01
|\ \ \ \
* | | | | Change Implicit Arguments to Arguments in test-suiteGravatar Jasper Hugunin2018-03-30
| | | * | Fix #6770: fixpoint loses locality info in proof mode.Gravatar Gaëtan Gilbert2018-03-29
* | | | | Fix #6631: Derive Plugin gives "Anomaly: more than one statement".Gravatar Pierre-Marie Pédrot2018-03-29
| |_|/ / |/| | |
| * | | Supporting fix/cofix in Ltac pattern-matching (wish #7092).Gravatar Hugo Herbelin2018-03-28
|/ / /
| | * Fixing #5547 (typability of return predicate in nested pattern-matching).Gravatar Hugo Herbelin2018-03-27
| | * Fixing #5500 (missing test in return clause of match leading to anomaly).Gravatar Hugo Herbelin2018-03-27
| |/ |/|
| * Fixes #7011 (Fix/CoFix were not considered in tactic unification).Gravatar Hugo Herbelin2018-03-26
|/
* Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
* Merge PR #6895: [compat] Remove "Refolding Reduction" option.Gravatar Maxime Dénès2018-03-09
|\
* | More examples about shelve/given_up in tactic-in-terms.Gravatar Hugo Herbelin2018-03-08
* | Proof engine: support for nesting tactic-in-term within other tactics.Gravatar Hugo Herbelin2018-03-08
| * [compat] Remove "Refolding Reduction" option.Gravatar Emilio Jesus Gallego Arias2018-03-08
|/
* Merge PR #6899: [compat] Remove "Standard Proposition Elimination"Gravatar Maxime Dénès2018-03-08
|\
* \ Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Gravatar Maxime Dénès2018-03-08
|\ \
* \ \ Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`Gravatar Maxime Dénès2018-03-07
|\ \ \
* \ \ \ Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)Gravatar Maxime Dénès2018-03-07
|\ \ \ \
| | | * | ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Gravatar Enrico Tassi2018-03-06
* | | | | Merge PR #6896: [compat] Remove NOOP deprecated options.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6824: Remove deprecated options related to typeclasses.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \ | |_|_|_|/ / |/| | | | |
| | | * | | Sanitize universe declaration in Context (stop using a ref...)Gravatar Gaëtan Gilbert2018-03-05
| | * | | | [compat] Remove NOOP and alias deprecated options.Gravatar Emilio Jesus Gallego Arias2018-03-04
| | |/ / /
| * / / / Remove deprecated options related to typeclasses.Gravatar Théo Zimmermann2018-03-04
| |/ / /
| | * / ssr: add Prenex Implicits for Some_inj to use it as a viewGravatar Anton Trunov2018-03-04
| |/ /
* | | Merge PR #935: Handling evars in the VMGravatar Maxime Dénès2018-03-04
|\ \ \ | |/ / |/| |
* | | Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \ \
| | * | Removing test for bug #2850.Gravatar Pierre-Marie Pédrot2018-03-03
| | | * [compat] Remove "Standard Proposition Elimination"Gravatar Emilio Jesus Gallego Arias2018-03-03
| | |/
| * | Remove 8.5 compatibility support.Gravatar Théo Zimmermann2018-03-02
| * | Remove VOld compatibility flag.Gravatar Théo Zimmermann2018-03-02
| |/
* / Fix #6878: univ undefined for [with Definition] bad instance size.Gravatar Gaëtan Gilbert2018-03-01
|/
* Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).Gravatar Maxime Dénès2018-02-24
|\
* \ Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`Gravatar Maxime Dénès2018-02-21
|\ \
* \ \ Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)Gravatar Maxime Dénès2018-02-21
|\ \ \
* \ \ \ Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just the...Gravatar Maxime Dénès2018-02-21
|\ \ \ \
| | | | * Fixes bug #6774 (anomaly with ill-typed template polymorphism).Gravatar Hugo Herbelin2018-02-20
| |_|_|/ |/| | |
| | * | Adding a test for wish #5532.Gravatar Hugo Herbelin2018-02-20
| |/ / |/| |
| * | Fix #6529: nf_evar_info and check the env evars' not just the conclGravatar Matthieu Sozeau2018-02-19
| | * Extend `zify_N` with knowledge about `N.pred`Gravatar Joachim Breitner2018-02-14
| |/ |/|
* | Merge PR #6713: Fix #6677: Critical bug with VM and universesGravatar Maxime Dénès2018-02-14
|\ \ | |/ |/|
| * Add test case for #6677.Gravatar Maxime Dénès2018-02-12
* | Merge PR #1047: Support universe instances on the literal TypeGravatar Maxime Dénès2018-02-12
|\ \ | |/ |/|
* | Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Gravatar Maxime Dénès2018-01-31
|\ \
* | | Add test case for #5286.Gravatar Maxime Dénès2018-01-29
| | * Support universe instances on the literal TypeGravatar Tej Chajed2018-01-26
| |/ |/|
* | Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Gravatar Maxime Dénès2018-01-22
|\ \
* \ \ Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.Gravatar Maxime Dénès2018-01-22
|\ \ \
| * | | Add test-suite file for issue #6617.Gravatar Cyprien Mangin2018-01-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 20:06:28 +0000