Merge pull request #3381 from aleksnanevski/master

changed coq-htt-core to work with rocq 9.0

Author: palmskog

Diff for: released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam

@@ -21,7 +21,7 @@ This library relies on propositional and functional extentionality axioms."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.19" & < "9.1~"}
+  "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") }
   "coq-hierarchy-builder" { (>= "1.7.0" & < "1.9~") | (= "dev") }
   "coq-mathcomp-algebra" 

Diff for: released/packages/coq-htt-core/coq-htt-core.2.1.0/opam

@@ -30,7 +30,7 @@ that HTT implements Separation logic as a shallow embedding in Coq."""
 build: [make "-C" "htt" "-j%{jobs}%"]
 install: [make "-C" "htt" "install"]
 depends: [
-  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
+  "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 

Diff for: released/packages/coq-htt/coq-htt.2.1.0/opam

@@ -30,7 +30,7 @@ that HTT implements Separation logic as a shallow embedding in Coq."""
 build: [make "-C" "examples" "-j%{jobs}%"]
 install: [make "-C" "examples" "install"]
 depends: [
-  "coq" {>= "8.19" & < "9.1~"}
+  "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup"