aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2019-01-29Update update-compat.py scriptJason Gross
It now removes the outdated `CompatOldOldFlag.v` file on `--release`, and it now correctly updates `bug_9166.v` which seems to specifically be about the compat flag behavior. Additionally, it inserts an "autogenerated" notice at top of the two bug files, and makes them read-only.
2019-01-29Merge PR #9274: Make `Instance` without a body always open a proofEnrico Tassi
Reviewed-by: gares Reviewed-by: mattam82 Reviewed-by: ppedrot
2019-01-29Merge PR #9383: Remove travisVincent Laporte
Reviewed-by: Zimmi48 Reviewed-by: vbgl
2019-01-28Merge PR #9341: [ssr] uniform clear disciplineMaxime Dénès
Reviewed-by: CohenCyril Ack-by: Zimmi48 Ack-by: gares Reviewed-by: maximedenes
2019-01-27[test] for bug #9385Enrico Tassi
2019-01-27Merge PR #9214: Notations: Removing useless parentheses on abbreviations ↵Emilio Jesus Gallego Arias
shortening a strict prefix of an application Reviewed-by: ejgallego
2019-01-25Merge PR #8637: Update -compat to support -compat 8.10Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares
2019-01-25Notations: Removing useless parentheses on abbrevs for prefix of an application.Hugo Herbelin
2019-01-24Merge PR #9325: Stop [Print] from saying [is (not) universe polymorphic].Hugo Herbelin
Reviewed-by: maximedenes
2019-01-24Update -compat to support -compat 8.10Jason Gross
This commit was created via `./dev/tools/update-compat.py --master`
2019-01-24Make `Instance` without a body always open a proof.Maxime Dénès
2019-01-24Merge PR #9377: [CS] recognize applied primitive projections as keys (fix #9375)Matthieu Sozeau
Ack-by: SkySkimmer Ack-by: gares Reviewed-by: mattam82 Ack-by: ppedrot
2019-01-23Merge PR #9270: Turn `Refine instance Mode` off by defaultPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: maximedenes Reviewed-by: ppedrot
2019-01-23Merge PR #9337: Fixing #9329: registering empty levels in the order they are ↵Emilio Jesus Gallego Arias
computed Reviewed-by: ejgallego
2019-01-22Remove travisGaëtan Gilbert
The azure OSX job replaces the first travis job, and the second always fails and so is useless.
2019-01-22Fixing #9329 (registering empty levels in the order they are recomputed).Hugo Herbelin
Was raising an anomaly 'Failure("Grammar.extend")' otherwise.
2019-01-22Make prvect tail recursive (fix #9355)Gaëtan Gilbert
Using a unit test as it's way faster than messing with universes. You can test with universes by ~~~coq Set Universe Polymorphism. Definition x1@{i} := True. Definition x2 := x1 -> x1. Definition x3 := x2 -> x2. Definition x4 := x3 -> x3. Definition x5 := x4 -> x4. Definition x6 := x5 -> x5. Definition x7 := x6 -> x6. Definition x8 := x7 -> x7. Definition x9 := x8 -> x8. Definition x10 := x9 -> x9. Definition x11 := x10 -> x10. Definition x12 := x11 -> x11. Definition x13 := x12 -> x12. Definition x14 := x13 -> x13. Definition x15 := x14 -> x14. Definition x16 := x15 -> x15. Definition x17 := x16 -> x16. Definition x18 := x17 -> x17. Definition x19 := x18 -> x18. About x19. (* 262144 universes *) ~~~ Note on my machine `About x18.` did not overflow even before this commit.
2019-01-22Turn `Refine Instance Mode` off by defaultMaxime Dénès
2019-01-22Make `Add Morphism` not rely on Refine InstanceMaxime Dénès
2019-01-22Distinguish ASTs for Instance and Declare InstanceMaxime Dénès
This makes code paths clearer (we still factorize a lot of the treatment), and we seize the opportunity to forbid anonymous `Declare Instance` which is not a documented construction, and seems to make little sense in practice.
2019-01-22[CS] recognize applied primitive projections as keys (fix #9375)Enrico Tassi
2019-01-19[ssr] compile "=> {x..} y" as "=> {x..y} y"Enrico Tassi
This is for consistency with "rewrite {x..} y"
2019-01-18[ssr] compile "=> {} y" as "=> {y} y"Enrico Tassi
2019-01-14Merge PR #9307: Handle local definitions in implicit arguments of InstanceMaxime Dénès
2019-01-09Stop [Print] from saying [is (not) universe polymorphic].Gaëtan Gilbert
[About] still says it. Close #9056.
2019-01-09Make some tests more robust by adding missing proof terminatorsMaxime Dénès
2019-01-09Test ltacprof in sequential modeMaxime Dénès
Scripting these commands in async mode does not really make sense.
2019-01-09Make it possible to pass flags to coq when running test suiteMaxime Dénès
2019-01-08Fix #9272: `Unset Nested Proofs Allowed` does not capture nested `Instance` ↵Maxime Dénès
proofs. We forbid commands that may open proofs inside proofs.
2019-01-08Merge PR #9292: Fixing some wrong scopes of variables in the interpretation ↵Emilio Jesus Gallego Arias
of the "in" clause of a "match"
2019-01-07Merge PR #9241: Fix #9240: Register for IDProp causes anomaly when non constantEnrico Tassi
2019-01-06Reworking error message for unresolved evar subterm of another evar.Hugo Herbelin
This is a reworking of 7fd28dc9: instead of using words such as "domain of", "codomain of" to refer to a position in the instance of the original evar, we simply display the instance and the name of the unresolved evar in this instance. This is both simpler and more informative. (The positional words remain useful for printing the evar_map in debugging though.) In passing, this fixes #8369 (Not_found in printing message about an unresolved subevar). Incidentally add possible breaking while printing "in environment".
2019-01-04Handle local definitions in implicit arguments of InstanceJasper Hugunin
2018-12-30Fixing an interpretation bug of the "in" clause of "match".Hugo Herbelin
- The head of "in" was wrongly considered binding - Aliases in the "in" pattern were not taken into account
2018-12-26Merge PR #8734: Make diffs work for more input stringsHugo Herbelin
2018-12-25Fixing printing bug due to using equality ill-checking hash key of kernel name.Hugo Herbelin
Thanks to Georges Gonthier for noticing it. Expanding a few Pervasives.compare at this occasion.
2018-12-22Merge PR #9248: Fix #7904: update proofview env after ltac constr:()Pierre-Marie Pédrot
2018-12-21Fix #9240: Register for IDProp causes anomaly when non constantGaëtan Gilbert
2018-12-21Do not exclude "opened" bugs from reportMaxime Dénès
2018-12-21Merge PR #9182: Stop printing Monomorphic/Polymorphic in Print.Maxime Dénès
2018-12-20Make diffs work for more input stringsJim Fehrle
Diff code uses the lexer to recognize tokens in the inputs, which can be Pp.t's or strings. To add the highlights in the Pp.t, the diff code matches characters in the input to characters in the tokens. Current code fails for inputs containing quote marks or "(*" because the quote marks and comments don't appear in the tokens. This commit adds a "diff mode" to the lexer to return those characters, making the diff routine more robust.
2018-12-20Merge PR #8488: Warning when using automatic template polymorphismPierre-Marie Pédrot
2018-12-20Merge PR #9200: [ssr] make `>` stand aloneMaxime Dénès
2018-12-19Fix #7904: update proofview env after ltac constr:()Gaëtan Gilbert
(in case of side effects) Also: Fix #4781 Fix #4496
2018-12-19Put #[universes(template)] in outputs testsGaëtan Gilbert
2018-12-19Merge PR #9231: Fixes #9229: Infix not robust wrt choice of variable names ↵Pierre-Marie Pédrot
in right-hand side
2018-12-18Merge PR #9223: Fix universe restriction in delayed mode.Pierre-Marie Pédrot
2018-12-18[ssr] make > a stand alone intro patternEnrico Tassi
2018-12-18Fixes #9229 (Infix not robust wrt choice of variable names).Hugo Herbelin
2018-12-18[ssr] new test by Arthur CharguéraudEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 20:23:26 +0000