12 Commits

Author	SHA1	Message	Date
Michael Goulet	d3e510eb9d	Don't ICE because recomputing overflow goals during find_best_leaf_obligation causes inference side-effects	2024-05-16 10:00:11 -04:00
lcnr	83e6da0be5	analyse visitor: build proof tree in probe	2024-05-09 17:29:53 +00:00
Michael Goulet	34e91ece90	Higher ranked goal source, do overflow handling less badly	2024-05-02 21:56:14 -04:00
Michael Goulet	3e03b1b190	Use a proof tree visitor to refine the Obligation for error reporting	2024-05-02 21:56:14 -04:00
lcnr	efa4269e54	move tests	2024-03-18 16:29:00 +01:00
lcnr	f26e1e8b63	NormalizesTo return nested goals	2024-03-18 15:53:16 +01:00
Oli Scherer	8206cffc48	Merge check_mod_impl_wf and check_mod_type_wf	2024-03-07 06:27:09 +00:00
lcnr	5ec9b8d778	distinguish recursion limit based overflow for diagnostics ... also change the number of allowed fixpoint steps to be fixed instead of using the `log` of the total recursion depth.	2024-02-29 10:14:02 +01:00
lcnr	2c7ede8f52	update tests	2024-02-26 10:57:46 +01:00
许杰友 Jieyou Xu (Joe)	ec2cc761bc	[AUTO-GENERATED] Migrate ui tests from // to //@ directives	2024-02-16 20:02:50 +00:00
Oli Scherer	83738a9b1c	Stop bailing out from compilation just because there were incoherent traits	2024-02-05 10:17:31 +00:00
lcnr	0947070871	consistently use "next solver" instead of "new solver"	2023-12-14 15:22:37 +01:00