444 Commits

Author	SHA1	Message	Date
Denis Merigoux	eec5ae54c6	Fixed formatting -> tests update	2023-05-04 19:18:53 +02:00
Denis Merigoux	bcd91f5dea	Merge branch 'master' into aides_logement_outre_mer	2023-05-04 11:04:28 +02:00
Louis Gesbert	5e26c5c83d	Yet more printer improvements ... - Fix the printer for scopes - Improve the printer for struct types - Remove `Print.expr'`. Use `Expr.format` as the function with simplified arguments instead.	2023-05-02 16:33:23 +02:00
Louis Gesbert	83e7a845fe	Cleanup expr printer interface ... - `Print.expr` no longer needs the context - This removes the need for `expr ~debug` + `expr_debug` ; use `Print.expr` for normal (non-debug) output, and `Print.expr' ?debug ()` for possibly debug output. - This improves consistency of debug expr output in many places - Prints simplified operators (without type suffix) in non-verbose mode (this patch also fixes some cases of `Expr.skip_wrappers` and leverages the binder equality provided by Bindlib)	2023-05-02 13:32:16 +02:00
Louis Gesbert	c249cef3cc	Printer: flatten nested let-ins too	2023-05-02 11:53:30 +02:00
Louis Gesbert	3e7a2a34ab	More printer improvements	2023-05-02 11:49:09 +02:00
Denis Merigoux	c6bafe8896	Update assets and tests	2023-05-02 10:58:45 +02:00
Denis Merigoux	7788bf9e73	Error message when two same states	2023-04-27 15:37:11 +02:00
Denis Merigoux	9b056f3ca1	Update assets and fix errors after rebase	2023-04-27 12:18:50 +02:00
Denis Merigoux	40af4d3a46	Disable optimization that was messing with the Proof backend	2023-04-27 12:13:18 +02:00
Denis Merigoux	7517894f77	Restore positions in test	2023-04-27 12:10:47 +02:00
Denis Merigoux	75c2a24b98	Changed position formatting	2023-04-27 12:09:22 +02:00
Denis Merigoux	19b33eaa96	Add lint and fix bugs related	2023-04-27 12:09:22 +02:00
Denis Merigoux	2d34fe7f27	Added a test related to #449	2023-04-27 12:09:22 +02:00
Denis Merigoux	081e60d2c6	Restore tests due to restored optimizations for default terms	2023-04-21 14:55:56 +02:00
Denis Merigoux	22b24a8634	Fusion of all optimizations done correctly	2023-04-21 12:32:09 +02:00
Denis Merigoux	f9a6644da3	Cleanliness and aesthetics	2023-04-18 15:45:30 +02:00
Denis Merigoux	4a1efcaa12	Restore tests and update assets	2023-04-18 14:46:25 +02:00
Denis Merigoux	0ec75ad589	Merge branch 'master' into adelaett-withoutexceptionsfix	2023-04-18 14:37:02 +02:00
Denis Merigoux	c5ba3e72fe	Restore CI	2023-04-18 09:59:24 +02:00
Denis Merigoux	ecccb5fb91	Last changes	2023-04-18 09:59:24 +02:00
adelaett	5d1f293fa0	finished looking at all tests	2023-04-14 18:27:20 +02:00
adelaett	70679b529b	adding some messages in new test files	2023-04-14 18:24:09 +02:00
adelaett	5e46253140	removed one remaning debuging print, and updating all the tests	2023-04-14 17:59:08 +02:00
adelaett	bc6e149618	same	2023-04-14 17:35:28 +02:00
adelaett	6f7d3422a4	more tests	2023-04-14 17:03:15 +02:00
adelaett	f3a5cbc5a8	test_typing err6 better error message	2023-04-14 16:37:27 +02:00
adelaett	a11ec6020e	commit not passing test about closure conversion	2023-04-14 16:34:37 +02:00
adelaett	e5d518af69	more fixing	2023-04-14 16:28:37 +02:00
adelaett	5f3584c94d	fixing more tests	2023-04-14 16:25:22 +02:00
adelaett	91805bfa43	fixing tests	2023-04-14 16:22:39 +02:00
adelaett	a9809b69a9	Merge branch 'master' into adelaett-withoutexceptionsfix	2023-04-14 11:19:58 +02:00
Louis Gesbert	e19e4af12d	Vastly improve the printer ... * fix lots of Format boxes * add parens based on precedence in the printer * fix interaction of Format and the colored line debug tags	2023-04-13 18:15:22 +02:00
adelaett	43c1fd9b7e	adding tests	2023-04-12 11:38:12 +02:00
alain	ec40de83fc	Merge branch 'master' into adelaett-withoutexceptionsfix	2023-04-06 13:57:22 +02:00
Denis Merigoux	ad02a0959d	Merge branch 'master' into aides_logement_outre_mer	2023-04-03 14:12:10 +02:00
Denis Merigoux	d147238088	Apply suggestions by @altgr	2023-04-03 13:42:14 +02:00
Denis Merigoux	e80143b3ca	Last linting pass and update tests	2023-03-31 17:56:45 +02:00
Denis Merigoux	5673708f36	Update assets	2023-03-31 15:34:51 +02:00
Denis Merigoux	3d86a12261	Update error messages	2023-03-31 14:01:04 +02:00
Denis Merigoux	04629f58cd	Merge branch 'master' into aides_logement_outre_mer	2023-03-30 15:14:06 +02:00
adelaett	6dee3874cc	Merge branch 'master' into adelaett-withoutexceptionsfix	2023-03-30 10:50:32 +02:00
Aymeric Fromherz	b85a199daa	Add support for let .. in constructions in Z3 backend (#434)	2023-03-29 06:41:40 +09:00
Aymeric Fromherz	8780a48312	Correct test invocations	2023-03-28 22:51:03 +09:00
Aymeric Fromherz	d0ef61219f	Add expected outputs for tests	2023-03-28 13:03:44 +09:00
Aymeric Fromherz	8fdd39d15a	Add negative test for let_in	2023-03-28 13:01:41 +09:00
Aymeric Fromherz	71ebd3a2c7	Test for Z3 let_in	2023-03-28 12:49:14 +09:00
Denis Merigoux	b801cccd15	Update tests	2023-03-21 13:32:38 +01:00
Denis Merigoux	aa8ab3be3d	Merge branch 'master' into c_backend	2023-03-21 12:14:10 +01:00
Denis Merigoux	b2d02f4b0f	Fixed all tests	2023-03-17 18:44:19 +01:00