15 Commits

Author	SHA1	Message	Date
MARCHE Claude	715fa89d16	separate transformations for intros, dequant, and remove_unused ... remove unused before reflection transformation avoid subst to a unused symbol	2023-04-25 12:20:08 +00:00
Claude Marche	91a8a26fde	fix obsolete sessions and one failed session	2023-02-07 12:25:21 +01:00
Jean-Christophe Filliatre	c891d2b87f	updated proof sessions	2022-09-08 16:00:29 +02:00
Claude Marche	db96723fd9	fix sessions	2022-07-07 15:49:23 +02:00
Claude Marche	ecb497d98a	Merge branch 'master' into eliminate_unused_symbols	2022-06-23 07:51:51 +02:00
Claude Marche	33115df1c9	fix sessions	2022-06-22 15:39:14 +02:00
Claude Marche	8abedf035e	fix sessions	2022-06-02 17:59:27 +02:00
Nightly Build	9e5eb47599	Vc: keep sp_if's splittable (and update sessions)	2022-05-02 18:29:28 +02:00
MARCHE Claude	c6f793011c	introduce_premises also "dequant" the let-ins	2022-04-21 16:23:20 +00:00
Jean-Christophe Filliatre	08712c15ac	micro-Python: added support for built-in function pow	2021-10-29 15:57:14 +02:00
Claude Marche	62e1037ff1	fix sessions	2021-09-03 11:59:11 +02:00
Claude Marche	cec915c4f1	fix obsolete sessions	2021-08-24 09:26:20 +02:00
Claude Marche	9674c541d7	fix session	2021-07-12 14:24:52 +02:00
Quentin Garchery	2513e6205f	Fix sessions	2021-06-10 11:55:05 +00:00
Jean-Christophe Filliatre	ee19cefd75	moved micro-C/Python examples from tests/ to examples/	2021-02-05 20:01:48 +01:00