1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
-R . CoqEAL
-arg -w -arg -projection-no-head-constant
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -notation-overridden
-arg -w -arg +duplicate-clear
-arg -w -arg +non-primitive-record
-arg -w -arg +undeclared-scope
-arg -w -arg +deprecated-hint-without-locality
-arg -w -arg +deprecated-hint-rewrite-without-locality
-arg -w -arg +deprecated-ident-entry
-arg -w -arg +deprecated-typeclasses-transparency-without-locality
-arg -w -arg -ambiguous-paths
-arg -w -arg +implicit-core-hint-db
theory/atomic_operations.v
theory/bareiss_dvdring.v
theory/bareiss.v
theory/binetcauchy.v
theory/closed_poly.v
theory/coherent.v
theory/companion.v
theory/dvdring.v
theory/edr.v
theory/fpmod.v
theory/frobenius_form.v
theory/gauss.v
theory/jordan.v
theory/kaplansky.v
theory/karatsuba.v
theory/minor.v
theory/mxstructure.v
theory/perm_eq_image.v
theory/polydvd.v
theory/rank.v
theory/similar.v
theory/smithpid.v
theory/smith.v
theory/smith_complements.v
theory/ssralg_ring_tac.v
theory/ssrcomplements.v
theory/strassen.v
theory/stronglydiscrete.v
theory/toomcook.v
refinements/hrel.v
refinements/param.v
refinements/refinements.v
refinements/pos.v
refinements/binnat.v
refinements/binint.v
refinements/poly_op.v
refinements/seqpoly.v
refinements/karatsuba.v
refinements/poly_div.v
refinements/binord.v
refinements/seqmx.v
refinements/seqmx_complements.v
refinements/hpoly.v
refinements/bareiss_eff.v
refinements/rational.v
refinements/boolF2.v
refinements/trivial_seq.v
refinements/examples/irred.v
refinements/binrat.v
refinements/multipoly.v
|
