package coq-mathcomp-ssreflect
  Compatibility package for rocq-mathcomp-ssreflect
Install
Dune Dependency
Authors
Maintainers
Sources
  
    
      mathcomp-2.4.0.tar.gz
    
    
        
    
  
  
  
    
  
        sha256=6307218d7e434fb6ffc81b9275c673d3f7f1f4884ad59b904abd205c437021a0
    
    
  Description
Published: 15 Apr 2025
Dependencies (2)
- 
  
    rocq-mathcomp-ssreflect
  
  
    = version
- coq-core
Dev Dependencies
None
Used by (46)
- 
  
    coq-comp-dec-modal
  
  
    >= "1.2"
- 
  
    coq-coqeal
  
  
    >= "2.0.0" & < "2.0.2" | >= "2.1.0"
- coq-coqeal-theory
- 
  
    coq-coquelicot
  
  
    >= "2.1.1" & < "3.1.0" | >= "3.3.1"
- 
  
    coq-deriving
  
  
    >= "0.2.2"
- coq-dijkstra
- 
  
    coq-disel-examples
  
  
    >= "2.3"
- 
  
    coq-extructures
  
  
    >= "0.5.0"
- 
  
    coq-fcsl-pcm
  
  
    >= "2.1.0"
- 
  
    coq-fourcolor
  
  
    >= "1.4.1"
- 
  
    coq-fourcolor-reals
  
  
    >= "1.4.1"
- 
  
    coq-gaia-numbers
  
  
    >= "2.0"
- 
  
    coq-gaia-ordinals
  
  
    >= "2.0"
- 
  
    coq-gaia-schutte
  
  
    >= "2.0"
- 
  
    coq-gaia-stern
  
  
    >= "2.0"
- 
  
    coq-gaia-theory-of-sets
  
  
    >= "2.0"
- 
  
    coq-graph-theory
  
  
    >= "0.9.6"
- 
  
    coq-graph-theory-planar
  
  
    >= "0.9.6"
- coq-hanoi
- 
  
    coq-htt
  
  
    >= "2.1.0"
- 
  
    coq-htt-core
  
  
    >= "2.1.0"
- 
  
    coq-infotheo
  
  
    >= "0.7.0" & != "0.7.5" & != "0.9.2"
- 
  
    coq-interval
  
  
    < "4.5.2" | >= "4.8.0"
- 
  
    coq-mathcomp-algebra-tactics
  
  
    >= "1.2.5"
- coq-mathcomp-bigenough
- 
  
    coq-mathcomp-classical
  
  
    >= "1.10.0"
- 
  
    coq-mathcomp-finmap
  
  
    = "2.2.0"
- 
  
    coq-mathcomp-multinomials
  
  
    >= "2.4.0"
- 
  
    coq-mathcomp-real-closed
  
  
    = "2.0.0" | >= "2.0.3"
- 
  
    coq-mathcomp-tarjan
  
  
    >= "1.0.3"
- 
  
    coq-mathcomp-word
  
  
    >= "3.2"
- 
  
    coq-mathcomp-zify
  
  
    >= "1.5.0+2.0+8.16"
- 
  
    coq-monae
  
  
    >= "0.7.0"
- coq-msets-extra
- coq-num-analysis
- 
  
    coq-plouffe
  
  
    >= "1.2.0"
- 
  
    coq-quickchick
  
  
    >= "1.1.0"
- 
  
    coq-regexp-brzozowski
  
  
    >= "1.2"
- 
  
    coq-reglang
  
  
    >= "1.2.2"
- 
  
    coq-ssprove
  
  
    >= "0.2.4"
- coq-trocq-hott-examples
- coq-type-infer
- coq-vellvm
- 
  
    coq-wasm
  
  
    >= "2.0.3"
- rocq-num-analysis-subset
- rocq-vellvm
Conflicts
None
 sectionYPositions = computeSectionYPositions($el), 10)"
  x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
  >
  
  
On This Page