coq/theories/setoid_ring, branch masterThe formal proof systemModify setoid_ring/Field_theory.v to compile with -mangle-names2020-12-16T02:17:58+00:00Jasper Hugunin2020-12-16T02:17:58+00:0096ad23e59418798fc5960940291ab5ea8b6330b4
Improve some error messages.2020-11-16T19:30:08+00:00Vincent Semeria2020-05-31T07:38:24+00:00f2a5096bf0829316eba869fe5d929337e6fd8bad
This also includes aligning with refman when relevant and using capital
letters and final period.
This also includes aligning with refman when relevant and using capital
letters and final period.
Modify setoid_ring/Ring.v to compile with -mangle-names2020-10-12T02:05:14+00:00Jasper Hugunin2020-10-09T22:49:42+00:00f136bcf5a067fcf1e38f48062ccde06875709e6a
Modify setoid_ring/InitialRing.v to compile with -mangle-names2020-10-12T02:05:14+00:00Jasper Hugunin2020-10-09T22:48:01+00:006b04433e6828112bfbd7914ca941912427f0e4ff
Modify setoid_ring/Ring_polynom.v to compile with -mangle-names2020-10-09T01:38:57+00:00Jasper Hugunin2020-10-09T01:38:57+00:00ef711580200fd216e544c37be715a6c8af157342
{new,setoid_}ring -> ring2020-10-02T11:23:30+00:00Maxime Dénès2020-09-18T12:15:18+00:004476f64dc87fb86738fc4c9f939113b70843c035
I believe this renaming makes it easier for new contributors to discover
the code of `ring`.
I believe this renaming makes it easier for new contributors to discover
the code of `ring`.
Modify setoid_ring/BinList.v to compile with -mangle-names2020-09-16T20:23:13+00:00Jasper Hugunin2020-09-13T04:03:31+00:00cc4494897f0897f5795c2bd25fc06d4b07c73667
Modify setoid_ring/Ring_theory.v to compile with -mangle-names2020-09-16T19:46:57+00:00Jasper Hugunin2020-09-13T01:04:01+00:002f670dce285c04c66729022b2b8b8ea65bba744b
Avoiding using a fixed introduction name in Ltac code of stdlib.2020-04-03T18:33:27+00:00Hugo Herbelin2020-03-22T11:30:55+00:00aa889ee516453af65bd74ffedf8ec3761f97eb43