aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
* 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
|/ /
| * Fix core hint database issue #6521Gravatar Anton Trunov2018-01-03
|/
* Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra...Gravatar Maxime Dénès2017-12-18
|\
* | Fix anomaly in [Type foo] command, + print uctx like Check.Gravatar Gaëtan Gilbert2017-12-11
| * use \ocaml macro in Extraction chapter; accept OCaml in Extraction LanguageGravatar Paul Steckler2017-12-05
|/
* Tests for global universe declarationsGravatar Matthieu Sozeau2017-12-01
* Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as in...Gravatar Maxime Dénès2017-11-30
|\
* \ Merge PR #6253: Fixing inconsistent associativity of level 10 in the table of...Gravatar Maxime Dénès2017-11-29
|\ \
| | * Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gravatar Gaëtan Gilbert2017-11-28
| |/ |/|
| * Fixing associativity registered for level 10.Gravatar Hugo Herbelin2017-11-27
* | Restrict universe context when declaring constants in obligations.Gravatar Gaëtan Gilbert2017-11-25
* | Fix interpretation of global universes in univdecl constraints.Gravatar Gaëtan Gilbert2017-11-25
* | In close_proof only check univ decls with the restricted context.Gravatar Gaëtan Gilbert2017-11-24
* | restrict_universe_context: do not prune named universes.Gravatar Gaëtan Gilbert2017-11-24
* | Stop exposing UState.universe_context and its Evd wrapper.Gravatar Gaëtan Gilbert2017-11-24
|/
* Fixing factorization of recursive notations in the case of an atomic separator.Gravatar Hugo Herbelin2017-11-20
* Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...Gravatar Maxime Dénès2017-11-20
|\
| * One more step in fixing #5762 ("where" clause).Gravatar Hugo Herbelin2017-11-14
* | Merge PR #922: New beta-iota compatibility refinementsGravatar Maxime Dénès2017-11-08
|\ \ | |/ |/|
* | Merge PR #1139: Add a linter.Gravatar Maxime Dénès2017-11-06
|\ \
| * | Put newlines at the end of files.Gravatar Gaëtan Gilbert2017-10-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 01:47:14 +0000