90 Commits

Author	SHA1	Message	Date
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
Paul Patault	171104e310	coma: expl attributes ... - move expl attributes inference from parser to typing - added possibility to give name to assertions	2024-08-08 09:06:08 +02:00
Paul Patault	ddb799e96d	coma: add attributes to pre/post if given in type decl	2024-08-08 09:06:08 +02:00
Paul Patault	2289c712c2	coma: fix lexer mli warning	2024-08-08 09:06:08 +02:00
Paul Patault	23f1a47aae	coma: proto let%attr let%file	2024-08-08 09:06:08 +02:00
Andrei Paskevich	b956a79701	coma: weird handlers (wip)	2024-08-08 09:06:08 +02:00
Andrei Paskevich	b8d7dabd30	coma: update examples/coma/asm.coma	2024-08-08 09:06:08 +02:00
Andrei Paskevich	a948e516bd	coma_logic: fix missing effects in mutully recursive definitions	2024-08-08 09:06:08 +02:00
Andrei Paskevich	df73ef05dc	coma: one barrier per cycle	2024-08-08 09:06:08 +02:00
Andrei Paskevich	06c41d6495	coma: minor	2024-08-08 09:06:08 +02:00
Andrei Paskevich	b220a78935	coma: do not precompute unneeded subVCs	2024-08-08 09:06:08 +02:00
Andrei Paskevich	a0929f218d	coma_typing: specced outcomes cannot appear before type or data parameters ... This is required to avoid illegal capture when desugaring.	2024-08-08 09:06:08 +02:00