search

jrh13 / hol-light

The HOL Light theorem prover
Other
435 stars 78 forks source link

Updating update_database.ml for OCaml 5 #95

Closed aqjune closed 1 month ago

aqjune commented 7 months ago

HOL Light is mostly working okay on OCaml 5, but features that require update_database.ml are still missing.

The placeholder file is here: https://github.com/jrh13/hol-light/blob/master/update_database_5.ml

SnarkBoojum commented 5 months ago

I had a look and pa_j.ml also needs an update.