aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while look...Gravatar Emilio Jesus Gallego Arias2018-04-09
|\
* \ Merge PR #7176: Fix #6956: Uncaught exception in bytecode compilationGravatar Pierre-Marie Pédrot2018-04-09
|\ \
* \ \ Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)Gravatar Maxime Dénès2018-04-09
|\ \ \
| | * | Fix #6956: Uncaught exception in bytecode compilationGravatar Maxime Dénès2018-04-06
* | | | Improve shell scriptsGravatar zapashcanon2018-04-05
* | | | Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.Gravatar Hugo Herbelin2018-04-04
|\ \ \ \ | |_|/ / |/| | |
* | | | Merge PR #6407: Fix #6404 - Print tactics called by ML tacticsGravatar Pierre-Marie Pédrot2018-04-04
|\ \ \ \
| | | * | ssr: check cleared hyps do exist (fix #7050)Gravatar Enrico Tassi2018-04-04
| |_|/ / |/| | |
* | | | Update coq_makefile timing testGravatar Jason Gross2018-04-02
| * | | Fix #6404 - Print tactics called by ML tacticsGravatar Jason Gross2018-04-02
|/ / /
* | | 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 #6257: anomaly with Printing Projections and Context.Gravatar Gaëtan Gilbert2018-03-30
| | | * Fixes #7110 ("as" untested while looking for notation for nested patterns).Gravatar Hugo Herbelin2018-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
| |/
* | Merge PR #7090: stm: don't propagate side effects when editing a proofGravatar Emilio Jesus Gallego Arias2018-03-28
|\ \
* \ \ Merge PR #6961: [test-suite] Add backtracking test for `Load`.Gravatar Enrico Tassi2018-03-28
|\ \ \
| | * | stm: don't propagate side effects when editing a proofGravatar Enrico Tassi2018-03-27
| | |/
* | / Slightly refining some error messages about unresolvable evars.Gravatar Hugo Herbelin2018-03-24
| |/ |/|
| * [test-suite] Add backtracking test for `Load`.Gravatar Emilio Jesus Gallego Arias2018-03-10
|/
* Merge PR #6946: Fix expected number of arguments for cumulative constructors.Gravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6949: Revert PR #873: New strategy based on open scopes for decidin...Gravatar Maxime Dénès2018-03-09
|\ \
| | * Fix expected number of arguments for cumulative constructors.Gravatar Gaëtan Gilbert2018-03-09
| |/ |/|
* | Merge PR #6775: Allow using cumulativity without forcing strict constraints.Gravatar Maxime Dénès2018-03-09
|\ \
| | * Revert "Merge PR #873: New strategy based on open scopes for deciding which n...Gravatar Maxime Dénès2018-03-09
| |/ |/|
| * Delayed weak constraints for cumulative inductive types.Gravatar Gaëtan Gilbert2018-03-09
| * Cumulativity: improve treatment of irrelevant universes.Gravatar Gaëtan Gilbert2018-03-09
| * Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
* | Merge PR #6480: Allow Prop as source for coercionsGravatar Maxime Dénès2018-03-09
|\ \ | |/ |/|
* | Merge PR #6895: [compat] Remove "Refolding Reduction" option.Gravatar Maxime Dénès2018-03-09
|\ \
| | * added test for coercion from typeGravatar charguer2018-03-09
| | * allow Prop as source for coercionsGravatar charguer2018-03-09
| |/ |/|
* | Merge PR #6945: Fix error with univ binders on monomorphic records.Gravatar Maxime Dénès2018-03-09
|\ \
* \ \ Merge PR #6155: Get rid of ' notation for Zpos in QArithGravatar Maxime Dénès2018-03-09
|\ \ \
* \ \ \ 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
|\ \ \ \ \ \ \ \
| | | | | | | | * [compat] Remove "Refolding Reduction" option.Gravatar Emilio Jesus Gallego Arias2018-03-08
| |_|_|_|_|_|_|/ |/| | | | | | |
| | | | | | | * Fix error with univ binders on monomorphic records.Gravatar Gaëtan Gilbert2018-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
|\ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 00:48:07 +0000