Pierre Roux
a162c0b8e6
rocqPackages.mathcomp: fix Coq shim selection
2026-08-18 15:39:38 +02:00
Théo Zimmermann
124e44e7fa
coqPackages: stop building from coq-packages.nix for >= 9
...
Introduce aliases.
coqPackages.rocq-core: introduce as alias of coq for Coq < 9
To facilitate the merging of coq-modules and rocq-modules derivations.
2026-08-18 15:39:37 +02:00
Théo Zimmermann
9ab29d8bf2
coqPackages: move remaining derivations to rocq-modules
2026-08-18 15:39:37 +02:00
Pierre Roux
8f7f02caad
rocqPackages.stdpp: merge with coqPackages.stdpp
2026-08-18 15:39:37 +02:00
Pierre Roux
e8ec89d76f
rocqPackages.stdlib: merge with coqPackages.stdlib
2026-08-18 15:39:37 +02:00
Pierre Roux
cc09ca4e4b
rocqPackages.relation-algebra: merge with coqPackages.relation-algebra
2026-08-18 15:39:37 +02:00
Pierre Roux
11b5a8d235
rocqPackages.parseque: merge with coqPackages.parseque
2026-08-18 15:39:36 +02:00
Pierre Roux
ffa34e2ae4
rocqPackages.mathcomp-real-closed: merge with coqPackages.mathcomp-real-closed
2026-08-18 15:39:36 +02:00
Pierre Roux
68c6508265
rocqPackages.mathcomp-finmap: merge with coqPackages.mathcomp-finmap
2026-08-18 15:39:36 +02:00
Pierre Roux
3ac2da7d31
rocqPackages.mathcomp-bigenough: merge with coqPackages.mathcomp-bigenough
2026-08-18 15:39:36 +02:00
Pierre Roux
1d597c0d8a
rocqPackages.mathcomp-analysis: merge with coqPackages.mathcomp-analysis
2026-08-18 15:39:36 +02:00
Pierre Roux
a38b849ba4
rocqPackages.iris: merge with coqPackages.iris
2026-08-18 15:39:35 +02:00
Pierre Roux
0f6109b799
rocqPackages.hierarchy-builder: merge with coqPackages.hierarchy-builder
2026-08-18 15:39:35 +02:00
Pierre Roux
853cde0e77
rocqPackages.mathcomp: merge with coqPackages.mathcomp
...
Make dependency on micromega-plugin optional for compatibility with
versions < 9.
2026-08-18 15:39:35 +02:00
Théo Zimmermann
c9dbdd6408
rocqPackages.bignums: merge with coqPackages.bignums
2026-08-18 15:39:35 +02:00
Pierre Roux
0efb0140f1
rocqPackages.stdlib: 9.1.0 -> 9.2.0
2026-07-24 15:46:43 +02:00
Pierre Roux
54f8f8a829
rocqPackages.micromega-plugin: 1.1.0 -> 1.1.1
2026-07-24 09:41:27 +02:00
Pierre Roux
1870911b32
rocqPackages.rocq-elpi: 3.4.0 -> 3.5.0
2026-07-24 08:37:01 +02:00
Pierre Roux
0de6221506
rocqPackages.mathcomp: 2.5.0 -> 2.6.0
2026-07-20 11:08:29 +02:00
Théo Zimmermann
1b950b50bd
rocqPackages.mkRocqDerivation: change prefix for rocq
...
Make the defauult prefix be set to `[ "rocq" ]` (instead of
`[ "rocq-core" ]`) if `useCoq` is `false`.
This matches the opam convention and ensures that the default
`opam-name` will be correct.
2026-07-15 21:43:39 +02:00
Cyril Cohen
cbe7fae921
rocqPackages.rocqnavi: init at 0.5.0
2026-06-27 13:33:21 +02:00
Pierre Roux
45906568b2
rocqPackages.hierarchy-builder: 1.10.2 -> 1.10.3
2026-06-25 10:08:15 +02:00
Vincent Laporte
f8a250e19b
rocqPackages.mathcomp-analysis: now depends on real-closed ( #532543 )
2026-06-17 14:35:15 +00:00
Pierre Roux
36d1ce50a7
rocqPackages.mathcomp-analysis: now depends on real-closed
2026-06-17 13:23:46 +02:00
Pierre Roux
499d913a1a
rocqPackage.mathcomp-real-closed: init at 2.0.5
2026-06-17 11:01:36 +02:00
Wolfgang Meier
c8d505b86e
rocqPackages.parseque: release v0.3.1
2026-06-17 10:42:09 +02:00
Vincent Laporte
e45516ba3b
rocqPackages.micromega-plugin: fix hash
2026-06-10 07:55:22 +02:00
Reynald Affeldt
a61e394343
rocqPackages.mathcomp-experimental-reals: update dependencies
2026-06-08 17:33:42 +09:00
Théo Zimmermann
ef3f1670a7
vsrocq-language-server: 2.3.4 → 2.4.3 ( #523053 )
2026-06-01 08:48:52 +00:00
SandaruKasa
9f822bb13b
rocqPackages.vsrocq-language-server: 2.3.4 -> 2.4.3
2026-05-30 14:52:42 +03:00
Pierre Roux
34725c072b
rocqPackages.micromega-plugin: 1.0.0 -> 1.1.0
2026-05-29 09:48:18 +02:00
Mysaa Java
bdf53214c6
rocqPackages.rocq-elpi: 3.3.0 -> 3.4.0
2026-05-22 14:49:57 +02:00
Pierre Roux
30b1c85e66
rocqPackages.mathcomp-algebra: master depends on micromega-plugin
2026-05-06 11:57:10 +02:00
Pierre Roux
2a7a765c10
rocqPackages.micromega-plugin: init at 1.0.0
2026-05-06 08:38:32 +02:00
Pierre Roux
96af9f8acf
rocqPackages.mathcomp: rename fingroup -> finite-group and character -> group-representation
2026-05-05 14:11:16 +02:00
Vincent Laporte
7017019bc1
rocqPackages.relation-algebra: enable for Rocq 9.1
2026-04-03 14:28:23 +02:00
Pierre Roux
13bfe0d63b
ocamlPackages.elpi: 3.6.1 -> 3.6.2
2026-03-23 08:26:06 +01:00
Pierre Roux
364777b471
rocqPackages.mathcomp-analysis: init at 1.16.0
2026-03-17 10:49:04 +01:00
Vincent Laporte
c42c1b9d97
rocqPackages.rocq-elpi: 3.2.0 -> 3.3.0 ( #499195 )
2026-03-12 12:37:41 +00:00
Pierre Roux
bb3d5ff0db
rocqPackages.rocq-elpi: 3.2.0 -> 3.3.0
2026-03-12 10:39:30 +01:00
Pierre Roux
ce85f4761e
rocqPackages.rocq-elpi: fix default elpi version
2026-03-12 10:25:08 +01:00
4ever2
18f99b1161
rocqPackages.iris: init at 4.5.0
2026-03-10 16:42:16 +01:00
4ever2
f136d4a6ec
rocqPackages.stdpp: init at 1.13.0
2026-03-09 13:49:40 +01:00
Mysaa Java
f753947c23
ocamlPackages.elpi: 3.4.2 -> 3.4.5
2026-02-25 19:02:57 +01:00
Pierre Roux
0344418644
rocqPackages.mathcomp-finmap: init at 2.2.2
2026-02-19 09:05:23 +01:00
Pierre Roux
6d859f6a8a
rocqPackages.mathcomp-bigenough: init at 1.0.4
2026-02-19 09:05:09 +01:00
Pierre Roux
396f67f973
rocqPackages.stdlib: 9.1.0 -> 9.2.0
2026-02-11 07:59:16 +01:00
Théo Zimmermann
b62a94ca89
Rocq platform 9.0 update ( #485359 )
2026-02-03 15:57:06 +00:00
Théo Zimmermann
28ced4eb9c
rocqPackages.relation-algebra: init at 1.8.0
2026-02-03 13:55:05 +01:00
Théo Zimmermann
4937cffd27
Update vsrocq ( #478436 )
2026-02-01 11:44:37 +01:00
