aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
* 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
* | | | Notations: Do not consider a non-occurring variable as a binder-only variable.Gravatar Hugo Herbelin2018-02-20
| | * | Implement name mangling optionGravatar Jasper Hugunin2018-02-17
* | | | Cleaner treatment of parameters in inferCumulativityGravatar Gaëtan Gilbert2018-02-16
| |/ / |/| |
| * | Fixing an anomaly in the presence of "let-in" in the type of a record.Gravatar Hugo Herbelin2018-02-13
|/ /
* | Use specialized function for inductive subtyping inference.Gravatar Gaëtan Gilbert2018-02-11
* | Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
* | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Maxime Dénès2018-01-18
|\ \
| * | Add a test that `prod_applist_assum` reduces the right number of let-insGravatar Jasper Hugunin2018-01-17
* | | Merge PR #6551: Bracket with goal selectorGravatar Maxime Dénès2018-01-16
|\ \ \ | |/ / |/| |
| * | More tests on brackets with goal selectors (including failures).Gravatar Théo Zimmermann2018-01-15
| * | Add test-suite file for bracket with goal selector.Gravatar Théo Zimmermann2018-01-15
* | | Force polymorphic definitions to have no internal constraints.Gravatar Pierre-Marie Pédrot2018-01-11
|/ /
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 20:46:52 +0000