add algebra tactics

affeldt-aist · affeldt-aist · commit 4ae9dc45632e · 2026-04-27T11:33:05.000+09:00
diff --git a/rocq-mathcomp-analysis.opam b/rocq-mathcomp-analysis.opam
@@ -19,6 +19,7 @@ depends: [
   "rocq-mathcomp-solvable"
   "rocq-mathcomp-field"
   "rocq-mathcomp-bigenough" { (>= "1.0.0") }
+  "rocq-mathcomp-algebra-tactics" { (>= "1.2.7") }
   "rocq-navi" {= "0.4.1" & with-doc}
 ]
 

Original file line number	Diff line number	Diff line change
`@@ -19,6 +19,7 @@ depends: [`
`19`	`19`	`"rocq-mathcomp-solvable"`
`20`	`20`	`"rocq-mathcomp-field"`
`21`	`21`	`"rocq-mathcomp-bigenough" { (>= "1.0.0") }`
	`22`	`+ "rocq-mathcomp-algebra-tactics" { (>= "1.2.7") }`
`22`	`23`	`"rocq-navi" {= "0.4.1" & with-doc}`
`23`	`24`	`]`
`24`	`25`