Merge pull request #1908 from affeldt-aist/opam_20250319

proux01 · web-flow · commit e9a12314ecaa · 2026-03-19T11:53:19.000+01:00
fix opam files
diff --git a/rocq-mathcomp-analysis-stdlib.opam b/rocq-mathcomp-analysis-stdlib.opam
@@ -19,6 +19,8 @@ depends: [
   "rocq-mathcomp-reals-stdlib"
 ]
 
+conflicts: [ "coq-mathcomp-analysis-stdlib" { < "1.16~" } ]
+
 tags: [
   "category:Mathematics/Real Numbers"
   "category:Mathematics/Real Calculus and Topology"
diff --git a/rocq-mathcomp-analysis.opam b/rocq-mathcomp-analysis.opam
@@ -21,6 +21,8 @@ depends: [
   "rocq-mathcomp-bigenough" { (>= "1.0.0") }
 ]
 
+conflicts: [ "coq-mathcomp-analysis" { < "1.16~" } ]
+
 tags: [
   "category:Mathematics/Real Calculus and Topology"
   "keyword:analysis"
diff --git a/rocq-mathcomp-classical.opam b/rocq-mathcomp-classical.opam
@@ -23,6 +23,8 @@ depends: [
   "rocq-hierarchy-builder" { (>= "1.8.0") }
 ]
 
+conflicts: [ "coq-mathcomp-classical" { < "1.16~" } ]
+
 tags: [
   "category:Mathematics/Logic/Classical logic"
   "keyword:classical logic"
diff --git a/rocq-mathcomp-experimental-reals.opam b/rocq-mathcomp-experimental-reals.opam
@@ -22,6 +22,8 @@ depends: [
   "rocq-mathcomp-bigenough" { (>= "1.0.0") }
 ]
 
+conflicts: [ "coq-mathcomp-experimental-reals" { < "1.16~" } ]
+
 tags: [
   "category:Mathematics/Real Numbers"
   "keyword:real numbers"
diff --git a/rocq-mathcomp-reals-stdlib.opam b/rocq-mathcomp-reals-stdlib.opam
@@ -20,6 +20,8 @@ depends: [
   "rocq-mathcomp-reals" { = version}
 ]
 
+conflicts: [ "coq-mathcomp-reals-stdlib" { < "1.16~" } ]
+
 tags: [
   "category:Mathematics/Real Numbers"
   "keyword:real numbers"
diff --git a/rocq-mathcomp-reals.opam b/rocq-mathcomp-reals.opam
@@ -18,6 +18,8 @@ depends: [
   "rocq-mathcomp-classical" { = version}
 ]
 
+conflicts: [ "coq-mathcomp-reals" { < "1.16~" } ]
+
 tags: [
   "category:Mathematics/Real Numbers"
   "keyword:real numbers"

Original file line number	Diff line number	Diff line change
`@@ -19,6 +19,8 @@ depends: [`
`19`	`19`	`"rocq-mathcomp-reals-stdlib"`
`20`	`20`	`]`
`21`	`21`
	`22`	`+conflicts: [ "coq-mathcomp-analysis-stdlib" { < "1.16~" } ]`
	`23`	`+`
`22`	`24`	`tags: [`
`23`	`25`	`"category:Mathematics/Real Numbers"`
`24`	`26`	`"category:Mathematics/Real Calculus and Topology"`
Original file line number	Diff line number	Diff line change
`@@ -21,6 +21,8 @@ depends: [`
`21`	`21`	`"rocq-mathcomp-bigenough" { (>= "1.0.0") }`
`22`	`22`	`]`
`23`	`23`
	`24`	`+conflicts: [ "coq-mathcomp-analysis" { < "1.16~" } ]`
	`25`	`+`
`24`	`26`	`tags: [`
`25`	`27`	`"category:Mathematics/Real Calculus and Topology"`
`26`	`28`	`"keyword:analysis"`
Original file line number	Diff line number	Diff line change
`@@ -23,6 +23,8 @@ depends: [`
`23`	`23`	`"rocq-hierarchy-builder" { (>= "1.8.0") }`
`24`	`24`	`]`
`25`	`25`
	`26`	`+conflicts: [ "coq-mathcomp-classical" { < "1.16~" } ]`
	`27`	`+`
`26`	`28`	`tags: [`
`27`	`29`	`"category:Mathematics/Logic/Classical logic"`
`28`	`30`	`"keyword:classical logic"`
Original file line number	Diff line number	Diff line change
`@@ -22,6 +22,8 @@ depends: [`
`22`	`22`	`"rocq-mathcomp-bigenough" { (>= "1.0.0") }`
`23`	`23`	`]`
`24`	`24`
	`25`	`+conflicts: [ "coq-mathcomp-experimental-reals" { < "1.16~" } ]`
	`26`	`+`
`25`	`27`	`tags: [`
`26`	`28`	`"category:Mathematics/Real Numbers"`
`27`	`29`	`"keyword:real numbers"`
Original file line number	Diff line number	Diff line change
`@@ -20,6 +20,8 @@ depends: [`
`20`	`20`	`"rocq-mathcomp-reals" { = version}`
`21`	`21`	`]`
`22`	`22`
	`23`	`+conflicts: [ "coq-mathcomp-reals-stdlib" { < "1.16~" } ]`
	`24`	`+`
`23`	`25`	`tags: [`
`24`	`26`	`"category:Mathematics/Real Numbers"`
`25`	`27`	`"keyword:real numbers"`
Original file line number	Diff line number	Diff line change
`@@ -18,6 +18,8 @@ depends: [`
`18`	`18`	`"rocq-mathcomp-classical" { = version}`
`19`	`19`	`]`
`20`	`20`
	`21`	`+conflicts: [ "coq-mathcomp-reals" { < "1.16~" } ]`
	`22`	`+`
`21`	`23`	`tags: [`
`22`	`24`	`"category:Mathematics/Real Numbers"`
`23`	`25`	`"keyword:real numbers"`