_CoqProject

-R theories mathcomp.apery
-R include mathcomp.apery
-arg -w -arg -notation-overridden
-arg -w -arg -ambiguous-paths
-arg -w -arg +local-declaration
-arg -w -arg +implicit-core-hint-db
-arg -w -arg +deprecated-hint-without-locality
-arg -w -arg +deprecated-hint-rewrite-without-locality
-arg -w -arg +deprecated-instance-without-locality
theories/a_props.v
theories/annotated_recs_b.v
theories/annotated_recs_c.v
theories/annotated_recs_d.v
theories/annotated_recs_s.v
theories/annotated_recs_v.v
theories/annotated_recs_z.v
theories/algo_closures.v
theories/arithmetics.v
theories/b_over_a_props.v
theories/b_props.v
theories/bigopz.v
theories/binomialz.v
theories/c_props.v
theories/extra_cauchyreals.v
theories/extra_mathcomp.v
theories/harmonic_numbers.v
theories/initial_conds.v
theories/ops_for_a.v
theories/ops_for_b.v
theories/ops_for_s.v
theories/ops_for_u.v
theories/ops_for_v.v
theories/posnum.v
theories/punk.v
theories/rat_of_Z.v
theories/reduce_order.v
theories/s_props.v
theories/seq_defs.v
theories/shift.v
theories/tactics.v
theories/z3irrational.v
theories/z3seq_props.v
theories/rho_computations.v
theories/multinomial.v
theories/hanson_elem_arith.v
theories/hanson_elem_analysis.v
theories/hanson.v