search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
630 stars 142 forks source link

fix master #1337

Closed digama0 closed 2 weeks ago

mn200 commented 2 weeks ago

I hope this is unnecessary given work in #1338

digama0 commented 2 weeks ago

I don't see how the first commit can be avoided, the current code seems plainly not well typed?

mn200 commented 2 weeks ago

For sake of future GitHub archaeologists: I fixed compile errors in a05c02a6e375865c85f2b489bdaf68d6ece4e942; theory problems in OpenTheory build have been fixed in pr #1338.