aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Merge PR #6747: Relax conversion of constructors according to the pCuIC modelGravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6328: Fix #6313: lost goals in nested ltac in refineGravatar Maxime Dénès2018-03-09
|\ \
* \ \ Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec valuesGravatar 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
| |/ / |/| |
* | | Merge PR #6522: Fix core hint database issue #6521Gravatar Maxime Dénès2018-03-08
|\ \ \
* \ \ \ Merge PR #6816: Adding mention of shelved/given-up status in Show ExistentialsGravatar Maxime Dénès2018-03-08
|\ \ \ \
* \ \ \ \ Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \
| | | | * | Fix SR breakage due to allowing fixpoints on non-rec valuesGravatar Matthieu Sozeau2018-03-08
| | | | | * Add test-suite file for cumulative constructorsGravatar Matthieu Sozeau2018-03-08
* | | | | | Merge PR #6899: [compat] Remove "Standard Proposition Elimination"Gravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \ | |_|_|_|_|/ |/| | | | |
* | | | | | Merge PR #6582: Mangle auto-generated namesGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6903: [compat] Remove "Shrink Abstract"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 #6790: Allow universe declarations for [with Definition].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
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | An experimental 'Show Extraction' command (grant feature wish #4129)Gravatar Pierre Letouzey2018-03-06
| | | | | * | | | | | | [compat] Remove "Shrink Abstract"Gravatar Emilio Jesus Gallego Arias2018-03-06
| |_|_|_|/ / / / / / / |/| | | | | | | | | |
* | | | | | | | | | | Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ...Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \ \ \ \ \ \
| | | | | * | | | | | | 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
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | |
| | | | | * | | | | | | | CHANGES and tests for with Definition @{univs}Gravatar Gaëtan Gilbert2018-03-05
| | | | * | | | | | | | | Sanitize universe declaration in Context (stop using a ref...)Gravatar Gaëtan Gilbert2018-03-05
| | | | |/ / / / / / / /
* | | | | | | | | | | | Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-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
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ...Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #915: Fix rewrite in * side conditionsGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | * | | | | | | | | Removing test for bug #2850.Gravatar Pierre-Marie Pédrot2018-03-03
| | | | * | | | | | | | | Adding a test file for evar handling in the VM.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
| | | * | | | | | | | Turn warning for deprecated notations on.Gravatar Théo Zimmermann2018-03-02
| | | |/ / / / / / /
| | * / / / / / / / Fix #6878: univ undefined for [with Definition] bad instance size.Gravatar Gaëtan Gilbert2018-03-01
| | |/ / / / / / /
| * / / / / / / / Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Gravatar Hugo Herbelin2018-03-01
| |/ / / / / / /
* / / / / / / / [test-suite] Add a basic test-case for `Load`.Gravatar Emilio Jesus Gallego Arias2018-02-28
|/ / / / / / /
* | | | | | | Merge PR #6756: Fix issue with spurious timing test failuresGravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinit...Gravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ |/| | | | | | |
| | | * | | | | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |_|/ / / / / |/| | | | | |
| | * | | | | [test-suite] Move sed scripts into bash arraysGravatar Jason Gross2018-02-24
* | | | | | | Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).Gravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6599: Decimals in preludeGravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \
| | | * | | | | | Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).Gravatar Hugo Herbelin2018-02-23
| |_|/ / / / / / |/| | | | | | |
| | | | | | * | Adding mention of shelved/given-up status in "Show Existentials".Gravatar Hugo Herbelin2018-02-22
| |_|_|_|_|/ / |/| | | | | |