Files

 master

/

theories

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

proux01

Adapt to math-comp/math-comp#1354

Feb 28, 2025

aaf1cdb · Feb 28, 2025

History

History

/

theories

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
a_props.v		a_props.v	rm warning caused by lacking archimedean	Nov 16, 2024
algo_closures.v		algo_closures.v	typos	Jan 24, 2025
annotated_recs_a.v		annotated_recs_a.v	Bump MathComp version to >= 1.12.0 (#3)	Dec 16, 2021
annotated_recs_b.v		annotated_recs_b.v	Bump MathComp version to >= 1.12.0 (#3)	Dec 16, 2021
annotated_recs_c.v		annotated_recs_c.v	Bump MathComp version to >= 1.12.0 (#3)	Dec 16, 2021
annotated_recs_d.v		annotated_recs_d.v	Bump MathComp version to >= 1.12.0 (#3)	Dec 16, 2021
annotated_recs_s.v		annotated_recs_s.v	Bump MathComp version to >= 1.12.0 (#3)	Dec 16, 2021
annotated_recs_v.v		annotated_recs_v.v	Bump MathComp version to >= 1.12.0 (#3)	Dec 16, 2021
annotated_recs_z.v		annotated_recs_z.v	Bump MathComp version to >= 1.12.0 (#3)	Dec 16, 2021
arithmetics.v		arithmetics.v	avoid all_algebra for finer deps	Nov 15, 2024
b_over_a_props.v		b_over_a_props.v	avoid all_algebra for finer deps	Nov 15, 2024
b_props.v		b_props.v	rm warning caused by lacking archimedean	Nov 16, 2024
bigopz.v		bigopz.v	adapt to MC#1256	Jan 22, 2025
binomialz.v		binomialz.v	rm warning caused by lacking archimedean	Nov 16, 2024
c_props.v		c_props.v	avoid all_algebra for finer deps	Nov 15, 2024
extra_cauchyreals.v		extra_cauchyreals.v	avoid all_algebra for finer deps	Nov 15, 2024
extra_mathcomp.v		extra_mathcomp.v	rm warning caused by lacking archimedean	Nov 16, 2024
hanson.v		hanson.v	avoid all_algebra for finer deps	Nov 15, 2024
hanson_elem_analysis.v		hanson_elem_analysis.v	avoid all_algebra for finer deps	Nov 15, 2024
hanson_elem_arith.v		hanson_elem_arith.v	avoid all_algebra for finer deps	Nov 15, 2024
harmonic_numbers.v		harmonic_numbers.v	avoid all_algebra for finer deps	Nov 15, 2024
initial_conds.v		initial_conds.v	avoid all_algebra for finer deps	Nov 15, 2024
multinomial.v		multinomial.v	Adapt to math-comp/math-comp#1354	Feb 28, 2025
ops_for_a.v		ops_for_a.v	Replace lia_tactics and field_tactics with mczify and Algebra Tactics	Apr 25, 2022
ops_for_b.v		ops_for_b.v	Ad-hoc fix for a performance issue	Apr 25, 2022
ops_for_nm_u.v		ops_for_nm_u.v	improved org	Dec 10, 2019
ops_for_s.v		ops_for_s.v	Remove 1.17.0 deprecations	Oct 13, 2023
ops_for_u.v		ops_for_u.v	Replace lia_tactics and field_tactics with mczify and Algebra Tactics	Apr 25, 2022
ops_for_v.v		ops_for_v.v	Replace lia_tactics and field_tactics with mczify and Algebra Tactics	Apr 25, 2022
posnum.v		posnum.v	adapt to MC#1256	Jan 22, 2025
punk.v		punk.v	avoid all_algebra for finer deps	Nov 15, 2024
rat_of_Z.v		rat_of_Z.v	avoid all_algebra for finer deps	Nov 15, 2024
rat_pos.v		rat_pos.v	avoid all_algebra for finer deps	Nov 15, 2024
reduce_order.v		reduce_order.v	avoid all_algebra for finer deps	Nov 15, 2024
rho_computations.v		rho_computations.v	Adapt to coq-community/coqeal#99	Jan 25, 2025
s_props.v		s_props.v	avoid all_algebra for finer deps	Nov 15, 2024
seq_defs.v		seq_defs.v	avoid all_algebra for finer deps	Nov 15, 2024
shift.v		shift.v	avoid all_algebra for finer deps	Nov 15, 2024
tactics.v		tactics.v	Port to MathComp 2	Oct 14, 2023
z3irrational.v		z3irrational.v	avoid all_algebra for finer deps	Nov 15, 2024
z3seq_props.v		z3seq_props.v	avoid all_algebra for finer deps	Nov 15, 2024
View all files