aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Merge PR #7237: [ssr] fix delayed clears (fix #7045)Gravatar Maxime Dénès2018-04-16
|\
* | [ltac] Deprecate nameless fix/cofix.Gravatar Emilio Jesus Gallego Arias2018-04-13
| * [ssr] fix delayed clears (fix #7045)Gravatar Enrico Tassi2018-04-13
|/
* Merge PR #7179: Fix #5981, bugs/opened/3263.v is non-deterministic by removin...Gravatar Jason Gross2018-04-12
|\
* \ Merge PR #500: Move bugs that have been closed on BugzillaGravatar Maxime Dénès2018-04-12
|\ \
* \ \ Merge PR #7087: Congruence tactic engine updateGravatar Pierre-Marie Pédrot2018-04-12
|\ \ \
| | * | Fix the status of some resolved bugsGravatar Tej Chajed2018-04-11
| |/ / |/| |
* | | 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
| | | | | * Fix #5981, bugs/opened/3263.v is non-deterministic by removing the test.Gravatar Théo Zimmermann2018-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
| | |/ /
| | | * Congruence: Fixing a bug with native projections.Gravatar Hugo Herbelin2018-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
|\ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 02:30:59 +0000