101 Commits

Author	SHA1	Message	Date
Benjamin Jorge	350cc165aa	Support module with interface in parsing API	2025-11-20 14:24:32 +01:00
Benjamin Jorge	667ab3ae79	Sandwich implementation	2025-11-20 14:14:24 +01:00
XIA Li-Yao	51e0579b35	Merge branch 'multi-spans' into 'master' ... coma: Highlight function call sites Closes #928 See merge request why3/why3!1261	2025-10-29 17:31:55 +01:00
XIA Li-Yao	061ff8cc12	Merge branch 'coma-errors-2' into 'master' ... coma: locate some error messages Closes #907 See merge request why3/why3!1260	2025-10-29 11:30:30 +01:00
Li-yao Xia	ea57d79058	coma: Allow annotating function calls with source locations	2025-10-17 20:23:04 +02:00
Li-yao Xia	f0d09ca4fd	coma: Track callers in VC generation	2025-10-17 20:23:04 +02:00
Li-yao Xia	b9a59a9ebb	coma: Add field for function call locations	2025-10-17 17:27:55 +02:00
Li-yao Xia	64b6266f58	coma: locate some error messages	2025-10-17 12:43:30 +02:00
Li-yao Xia	340fc7b46e	coma: better better type error messages	2025-10-17 11:13:17 +02:00
Paul Patault	7064223432	coma: typing better error messages	2025-10-17 10:37:47 +02:00
Andrei Paskevich	a5898d4657	coma_logic: ignore fake dependencies in mutually recursive handlers	2025-07-24 20:00:25 +02:00
Claude Marche	e991d73789	update headers	2025-06-04 10:51:30 +02: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
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
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
Paul Patault	bf775596c8	coma: generalize let%attr in let%span ... + creusot patches + CI patches	2024-08-08 11:09:30 +02:00