-
MARCHE Claude authored
replaced the 'variant {0}' by diverges to avoid unproved goals but now we have warnings. TO INVESTIGATE: uncomment the commented variants, that are supposed to work
5579ef01
replaced the 'variant {0}' by diverges to avoid unproved goals but now we have warnings. TO INVESTIGATE: uncomment the commented variants, that are supposed to work