aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
* Correct some spelling errorsmasterGravatar Benjamin Barenblat2018-07-22
* Remove fourier pluginGravatar Maxime Dénès2018-07-17
* Tactic deprecation machineryGravatar Maxime Dénès2018-07-12
* [test suite] Test case for attributesGravatar Vincent Laporte2018-07-03
* Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsGravatar Pierre-Marie Pédrot2018-07-03
|\
| * hints: add Hint Variables/Constants Opaque/Transparent commandsGravatar Matthieu Sozeau2018-07-02
* | Add test for Uniform Inductive ParametersGravatar Jasper Hugunin2018-07-01
|/
* Adding various tests for mutual records.Gravatar Pierre-Marie Pédrot2018-06-24
* Merge PR #6754: Better elaboration of pattern-matchings on primitive projectionsGravatar Pierre-Marie Pédrot2018-06-19
|\
| * Add test-suite case for performance, had to use TimeoutGravatar Matthieu Sozeau2018-06-15
| * Better elaboration of pattern-matchings on primitive projectionsGravatar Matthieu Sozeau2018-06-15
* | Do not allow spliting in res_pf, this is reserved for pretypingGravatar Matthieu Sozeau2018-06-15
|/
* Merge PR #7229: Deprecate implicit tactic solving.Gravatar Hugo Herbelin2018-06-04
|\
* \ Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.Gravatar Matthieu Sozeau2018-06-04
|\ \
| | * Deprecate implicit tactic solving.Gravatar Pierre-Marie Pédrot2018-06-04
| |/ |/|
* | Introduce an option to allow nested lemma, and turn it off by default.Gravatar Théo Zimmermann2018-05-17
* | Make "intro"/"intros" progress on existential variables.Gravatar Hugo Herbelin2018-05-02
* | Strict focusing using Default Goal Selector.Gravatar Gaëtan Gilbert2018-04-29
* | Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.Gravatar Hugo Herbelin2018-04-26
* | 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 #7087: Congruence tactic engine updateGravatar Pierre-Marie Pédrot2018-04-12
|\ \
* | | 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
| |/ |/|
| * Congruence: Fixing a bug with native projections.Gravatar Hugo Herbelin2018-03-27
|/
* 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
|\
| * 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
* | added test for coercion from typeGravatar charguer2018-03-09
* | allow Prop as source for coercionsGravatar charguer2018-03-09
|/
* Merge PR #6747: Relax conversion of constructors according to the pCuIC modelGravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6522: Fix core hint database issue #6521Gravatar Maxime Dénès2018-03-08
|\ \
* \ \ Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...Gravatar Maxime Dénès2018-03-08
|\ \ \
| | | * Add test-suite file for cumulative constructorsGravatar Matthieu Sozeau2018-03-08
| |_|/ |/| |
* | | Merge PR #6582: Mangle auto-generated namesGravatar Maxime Dénès2018-03-08
|\ \ \
| | * | 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
|\ \ \ \
* \ \ \ \ 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
|\ \ \ \ \ \
* \ \ \ \ \ \ 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
| | |/ / / / /
* | | | | | | Merge PR #935: Handling evars in the VMGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ | |_|/ / / / / |/| | | | | |
| * | | | | | Adding a test file for evar handling in the VM.Gravatar Pierre-Marie Pédrot2018-03-03
| | |_|_|/ / | |/| | | |
* / | | | | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Gravatar Hugo Herbelin2018-03-01
|/ / / / /
| * / / / Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/ / / /
* | | | Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 06:21:11 +0000