476 Commits

Author	SHA1	Message	Date
Johannes Kanig	e6c44bb771	Follow AST change in gnat2why	2025-11-12 10:48:43 +00:00
Johannes Kanig	a2807b3ddb	Merge 1.8.2 into AdaCore master	2025-10-14 10:32:03 +09:00
Claude Marche	e991d73789	update headers	2025-06-04 10:51:30 +02:00
Martin Clochard	d29be55424	Clean up compiler warnings ... Change-Id: Ibf6a012ed61635ea324cbabee05cadb72e143baf	2025-04-07 11:25:36 +02:00
Matteo Manighetti	399658bd65	Merge remote-tracking branch 'why3-inria/move_concrete_terms_out_of_parser' into why3-devel	2025-03-25 17:55:52 +01:00
Matteo Manighetti	f39e24ed74	Merge branch 'master' into why3-devel	2025-03-25 17:47:35 +01:00
Claude Marche	a912f9d0f7	fix conversion of term to concrete terms for records	2025-02-28 13:38:49 +01:00
Johannes Kanig	7a46b14d36	Adapt Why3 tree to gnat2why changes	2025-01-15 17:36:46 +09:00
Matteo Manighetti	c04b008016	Merge remote-tracking branch 'why3-inria/master' into why3-devel	2024-12-13 17:34:11 +01:00
Guillaume Melquiond	8a86d9ac62	Update copyright years.	2024-12-07 09:01:55 +01:00
Andrei Paskevich	5b9a766db5	coma: avoid splitting records when factorizing	2024-11-28 16:58:03 +01:00
Andrei Paskevich	d41309a7d3	coma: minor	2024-11-28 14:31:21 +01:00
Andrei Paskevich	128528db40	coma: ignore implicit imports for record splitting	2024-11-28 11:38:33 +01:00
Andrei Paskevich	379d56b1d7	coma: simplify record manipulations on the fly	2024-11-27 14:08:36 +01:00
Matteo Manighetti	dca6530002	Merge remote-tracking branch 'why3-inria/master' into why3-devel	2024-10-30 14:11:24 +01:00
Claude Marche	12d4122a41	Improve Mlw_printer for Eoptexn	2024-10-25 10:32:29 +02:00
Matteo Manighetti	1c65544ddb	Merge commit '1dc1b78e8c8e39e7b57e7299be0879ed027d19bd' into why3-before-cex-from-rac	2024-10-23 16:51:58 +02:00
Paul Patault	b7d4770c7d	coma: simplify examples	2024-10-17 20:00:12 +02:00
Claude Marche	35ef46abbf	make span file names relative to the file they appear into	2024-10-12 18:34:59 +02:00
MARCHE Claude	d1afe3fab8	CFG typing: locate exceptions raised by use/import ... Also ensures filenames in spans are relative to the file they occur in	2024-10-11 13:01:01 +02:00
Andrei Paskevich	1e5c04769f	coma: eval_match expects all the implicit module imports	2024-09-26 11:34:34 +02:00
Andrei Paskevich	f3a2f7cc34	coma: add Fany	2024-09-19 13:31:08 +02:00
Andrei Paskevich	79192cae28	coma: apply eval_match to VCs and inferred pre-/post-conditions	2024-09-19 13:28:03 +02:00
Andrei Paskevich	b6f9d81e2e	coma: replace levels with a neutrality status + protected handler set	2024-09-17 20:39:21 +02:00
Andrei Paskevich	a5024a38ce	coma: fix wrong levels in factorize and missing negations in t_neg	2024-09-17 12:20:23 +02:00