Kazuhiko Sakaguchi

icon indicating an email [email protected]

icon location Lyon, France icon location Postdoc in the Plume team at CNRS, ENS de Lyon, UCBL, LIP | Interests: interactive theorem proving, formalization of mathematics, and proof by reflection

Results 306 comments of Kazuhiko Sakaguchi

Split ssralg.v

Nix CI looks a bit unstable right now, but real-closed is an actual breakage: ``` File "./theories/ordered_qelim.v", line 443, characters 13-18: Error: The variable add0r was not found in the...

Split ssralg.v

Apparently, `ordered_qelim.v` depends on the reflection stuff defined in `ssralg.v` and thus imports `GRing`. So I probably need to reexport the `GRing` modules for the time being.

Split ssralg.v

I'm taking advantage of this PR to isolate the deprecation stuff in `ssralg.v`. Since the largest file (`algebra.v`) is 4.5k lines long, I'm already quite happy with the result.

Split ssralg.v

I introduced a new file `alg_theory/decfield.v` for `decFieldType` and `closedFieldType`, and updated the description of the PR.

Split ssralg.v

This PR is ready. I will add changelog entries.

Split ssralg.v

I renamed `alg_theory` to `alg`.