Paul Patault
6e847f2de7
coma: apply updated syntax in tests
2025-08-27 11:45:58 +02:00
Paul Patault
000fd2d347
coma: update stdlib + examples
2024-08-08 11:09:46 +02:00
Andrei Paskevich
4ab78a9f61
coma: eliminate trivial equalities more aggressively
2024-08-08 09:06:08 +02:00
Andrei Paskevich
6be7f4230d
coma: minor
2024-08-08 09:06:08 +02:00
Andrei Paskevich
55ce2c0219
coma_vc: minor fix
2024-08-08 09:06:07 +02:00
Paul Patault
c650e9ee2c
coma: separation let / letrec
2024-08-08 09:06:07 +02:00
Andrei Paskevich
197b364288
coma: subgoal factorization back online (disable with a debug flag)
...
+ use explicit context argument in the vc_* calls
+ change c_glob on Eany, make sure the topmost Eany is done last
2024-08-08 09:06:07 +02:00
Paul Patault
66d39526c1
coma: syntax update && polymorphism (wip)
2024-08-08 09:06:07 +02:00
Xavier Denis
e4d141629c
Add regression test
2023-04-25 11:57:38 +02:00
Xavier Denis
46dd6d5abd
Fix return and absurd parsing in MLCFG modules
...
Inside an MLCFG module it was not possible to use `return` or `absurd`
inside normal MLW declarations. This fixes the issue by changing how
blocks are parsed.
2021-02-09 17:57:11 +01:00
Xavier Denis
49a85e580f
move cfg tests from tests/ to examples/
2021-02-05 17:45:09 +01:00
Claude Marché
22d325ab85
new headers
2010-12-13 16:15:08 +01:00
François Bobot
13ae52d0d8
Plugin inside whyconf file
2010-12-01 13:05:55 +01:00
Francois Bobot
1cedcd8cf5
simplify_array en tant que transformation builtin au lieu de plugin
2010-07-06 14:26:59 +00:00
Andrei Paskevich
b3d1d542b1
rework configure:
...
- no more version.sh, use config.ml.in and version.tex.in instead
- dynlink compatibility is moved to config.ml
- comment out unused sections in Makefile
- provide the explicit --enable-ide option
- provide the explicit --enable-plugins option
- require at least Ocaml 3.10
- remove *-yes and *-no targets from Makefile,
use ifeq() instead
2010-04-17 13:07:08 +00:00
Francois Bobot
3d5022d024
bench_plugins : mise à jour des plugins
2010-03-24 14:56:43 +00:00
Jean-Christophe Filliâtre
1c4e78f52f
module Pattern
2010-03-22 11:52:38 +00:00
Francois Bobot
3a2b06b65f
driver utilise register
2010-03-18 06:59:45 +00:00
Francois Bobot
c9f1ab6b09
driver utilise maintenant en interne des context list Transform.t
...
dans les drivers il n'y a qu'une seul liste de transformations
2010-03-16 10:07:52 +00:00
Andrei Paskevich
fc2f7b50c8
move find_ts/find_ls/find_pr functions to Theory,
...
provide ns_find_prop and ns_find_fmla for convenience
2010-03-15 23:45:07 +00:00
Francois Bobot
09d9960f58
Ajoiut des context list t dans transform
2010-03-15 23:19:07 +00:00
Francois Bobot
c70a9c3811
- Ajout de split_conjunction
...
- Ajout du choix d'appliquer les transformations avant ou après la séparation
en un but par contexte (certainement à modifier)
- Ajout de quelques transformations et plugins
- ajout des options list-printers et list-transforms
2010-03-14 16:54:15 +00:00
Francois Bobot
3cb0ff15e5
Pour compiler les plugins
2010-03-12 23:59:26 +00:00
Francois Bobot
d49c181bf4
Ajout d'une proposition pour les transformations et les plugins dans les drivers
2010-03-12 23:21:57 +00:00
