math-comp / finmap

Finite sets, finite maps, multisets and generic sets

The Mathematical Components repository

The Mathematical Components Library is an extensive and coherent repository of formalized mathematical theories. It is based on the Coq proof assistant, powered with the Coq/SSReflect language.

These formal theories cover a wide spectrum of topics, ranging from the formal theory of general purpose data structures like lists, prime numbers or finite graphs, to advanced topics in algebra. The repository includes the foundation of formal theories used in a formal proof of the Four Colour Theorem (Appel - Haken, 1976) and a mechanization of the Odd Order Theorem (Feit - Thompson, 1963), a landmark result of finite group theory, which utilizes the library extensively.

Installation

If you already have OPAM installed (a fresh or up to date version of opam 2 is required):

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-ssreflect

Additional packages go by the name of coq-mathcomp-algebra, coq-mathcomp-field, etc... See INSTALL for detailed installation instructions in other scenarios.

How to get help

• The website of the MathComp library contains:
  • links to the HTML documentation of the last version as well as the documentation of previous versions,
  • a list of tutorials
• The ssreflect mailing list is the primary venue for help and questions about the library.
• The Mathematical Components Book provides a comprehensive introduction to the library.
• Experienced users hang around at StackOverflow listening to the ssreflect and coq tags.

Publications and Tools using MathComp

A collection of papers using the Mathematical Components library

finmap's Issues

totalType in ProdLexOrder and SeqProdOrder

Definitions of latticeType and totalType are identical in the modules ProdLexOrder and SeqProdOrder:

finmap/order.v

Lines 3466 to 3467 in dd86e52

	Canonical latticeType := LatticeType (T * T') total.
	Canonical totalType := LatticeType (T * T') total.

finmap/order.v

Lines 3640 to 3642 in dd86e52

	Canonical latticeType := LatticeType (seq T) total.
	Canonical blatticeType := BLatticeType (seq T) (BLattice.Mixin le0x).
	Canonical totalType := LatticeType (seq T) total.

Probably you mean Canonical orderType := OrderType (T * T') total and Canonical orderType := OrderType (seq T) total, respectively?

Missing coercion from finSet to finType

It'd be nice if fset_sub_finType would be made a coercion.

Coercion fset_sub_finType : finSet >-> finType.

Which version works with mathcomp 1.9? and the upcoming?

I have several projects depending on finmap and dependencies are difficult to track.

In particular, which is the version to use for compiling multinomials, in the ultimate goal of compiling CoqEAL? See the issue posted there.

Reverse/Dual/Opposite of an order

Note on what we discussed at Dagstuhl 18341:

• The name "reverse" order looks bad to me. Indeed the reverse lexicographic order is not the reverse of the lex order. My vote goes for "dual". "opposite" is also ok.
• dual of finite (porder/order/lattice) should be canonically finite.

Cheers,

Florent

finmap for 1.12?

the current 1.5.0 fails on

File "./set.v", line 764, characters 7-23:
Error: Cannot apply lemma join_idPr

Bigop support

It would be great to have bigop support in the library. Here's a preliminary set of bigops I use:

Open Scope fset_scope.

Notation "\bigcup_ ( i <- r | P ) F" :=
  (\big[@fsetU _/fset0]_(i <- r | P%fset) F%fset) : fset_scope.

Notation "\bigcup_ ( i <- r ) F" :=
  (\big[@fsetU _/fset0]_(i <- r) F%fset) : fset_scope.

Notation "\bigcup_ ( i | P ) F" :=
  (\big[@fsetU _/fset0]_(i | P) F%fset) : fset_scope.

Notation "\bigcup_ ( i 'in' A | P ) F" :=
  (\big[@fsetU _/fset0]_(i in A | P) F%fset) : fset_scope.

Notation "\bigcup_ ( i 'in' A ) F" :=
  (\big[@fsetU _/fset0]_(i in A) F%fset) : fset_scope.

Section FSetMonoids.

Import Monoid.
Variable (T : choiceType).

Canonical fsetU_monoid := Law (@fsetUA T) (@fset0U T) (@fsetU0 T).
Canonical fsetU_comoid := ComLaw (@fsetUC T).

End FSetMonoids.

Section BigFOpsFin.

Variables (T : choiceType) (I : finType).
Implicit Types (P : pred I) (A B : {fset I}) (F :  I -> {fset T}).

Lemma bigfcup_sup j P F : P j -> F j `<=` \bigcup_(i | P i) F i.
Proof. by move=> Pj; rewrite (bigD1 j) //= fsubsetUl. Qed.

Lemma bigfcupP x F P :
  reflect (exists2 i : I, P i & x \in F i) (x \in (\bigcup_(i | P i) F i)).
Proof.
apply: (iffP idP) => [|[i Pi]]; last first.
  apply: fsubsetP x; exact: bigfcup_sup.
by elim/big_rec: _ => [|i _ Pi _ /fsetUP[|//]]; [rewrite in_fset0 | exists i].
Qed.

Lemma bigfcupsP (U : {fset T}) P F :
  reflect (forall i : I, P i -> F i `<=` U)
          (\bigcup_(i | P i) F i `<=` U).
Proof.
apply: (iffP idP) => [sFU i Pi| sFU].
  by apply: fsubset_trans sFU; apply: bigfcup_sup.
by apply/fsubsetP=> x /bigfcupP[i Pi]; apply: (fsubsetP (sFU i Pi)).
Qed.

End BigFOpsFin.

Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03

The Coq team released Coq 8.17+rc1 on December 29th, 2022 and plans to release Coq 8.17.0 around March 7th, 2023.
The corresponding Coq Platform release 2023.03 should be released before April 14th, 2023.
It can be delayed in case of difficulties until June 30, 2023, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.17+rc1.

Coq Platform CI is currently testing opam package coq-mathcomp-finmap.1.5.2
from official repository https://coq.inria.fr/opam/released/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.1.5.2/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2023.03, please inform us as soon as possible and before March 21st, 2023!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.17~2023.03+preview1 which already supports Coq version 8.17+rc1 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#335

Not compatible with Coq.8.7

When trying to compile I get the following error.

git clone [email protected]:math-comp/finmap.git;
cd finmap;
make

which leads to:

File "./finmap.v", line 2309, characters 0-72:
Error:
Ltac call to "by (ssrhintarg)" failed.
Conversion test raised an anomalyAnomaly
                                 "Universe mathcomp.finmap.finmap.1389 undefined."
                                 Please report at http://coq.inria.fr/bugs/.

Admitting the lemma, leads to the following:

File "./finmap.v", line 2444, characters 0-63:
Error:
Ltac call to "by (ssrhintarg)" failed.
Conversion test raised an anomalyAnomaly
                                 "Universe mathcomp.finmap.finmap.1564 undefined."
                                 Please report at http://coq.inria.fr/bugs/.

Should "unit_irrelevance" fact be moved elsewhere?

Does it make sense to move unit_irrelevance elsewhere in Coq's part of ssreflect or mathcomp?

E.g. to ssrfun, near unitE lemma, which in turn could be used to prove the fact:

Fact unit_irrelevance (x y : unit) : x = y.
Proof. by rewrite !unitE. Qed.

Simplification in imset2 should be locked

Consider the following code:

Variable (f1 f2 : {fset nat}).
Lemma bla : [fset (n1 + n2)%N | n1 in f1, n2 in f2] == fset0.
Proof.
rewrite /=.

Then the goal is:

  f1, f2 : {fset nat}
  ============================
  Imfset.imfset2 imfset_key (K:=nat_choiceType) (T1:=nat_choiceType)
    (T2:=fun _ : nat => nat_choiceType) (fun n1 : nat => [eta addn n1])
    (p1:=mem_fin (fin_finpred (pT:=fset_finpredType nat_choiceType) f1))
    (p2:=fun _ : nat =>
         mem_fin (fin_finpred (pT:=fset_finpredType nat_choiceType) f2))
    (Phantom (mem_pred nat) (mem f1))
    (Phantom (nat -> mem_pred nat) (fun _ : nat => mem f2)) == fset0

Which is completely unreadable. I think the simplification should not be possible except after some form of unlocking.

About the lemma naming prefix `f`.

Almost all lemmas in finmap are named following finset but prefixed with a f. Thus, setUP becomes fsetUP, etc...

However, I'm not sure this is the best approach; why not use the same names? The user could use Coq namespaces to select between the two.

My motivation is that I have many proofs that go basically unchanged between set and fset but for the prefix. See for instance #1, the proof of bigfcup_sup is exactly the same than in finset.v but for the name [the same applies for all other lemmas in that issue].

From mathcomp Require Import order...

...in set.v seems dubious (especially given the -R mathcomp.finmap flag)

In any case, as long as the library is not release, this makes it difficult to add it as an external project in other developments.

"ge 0" does not type check

Hello,

While "le 0" (or equivalently, ">= 0") type checks, "ge 0" (or "<= 0") does not.

Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import all_ssreflect.
Require Import order.
Import Order.Def Order.Syntax Order.Theory.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Local Open Scope order_scope.

Section OrderTest.

Check le 0.                   (* or (>= 0) *)
Fail Check ge 0.              (* or (<= 0) *)
(* Toplevel input, characters 24-25: *)
(* > Check ge 0. *)
(* >          ^ *)
(* Error: *)
(* The term "0" has type "nat" while it is expected to have type *)
(*  "porderType ?display". *)

End OrderTest.

Please pick the version you prefer for Coq 8.15 in Coq Platform 2022.02

The Coq team released Coq 8.15.0 on January 13, 2022.
The corresponding Coq Platform release 2022.02 should be released before February 28, 2022.
It can be delayed in case of difficulties until April 11, 2022, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.15.0.

Coq Platform CI is currently testing opam package coq-mathcomp-finmap.1.5.1
from official repository https://coq.inria.fr/opam/released/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.1.5.1/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2022.02, please inform us as soon as possible and before February 14, 2022!

The working branch of Coq Platform, which already supports Coq version 8.15.0, can be found here https://github.com/coq/platform/tree/main.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#193

Need `Coq.Program.Tactics.`

In Coq 8.14 (rc1), I am getting this:

File "./finmap/finmap.v", line 752, characters 0-186:
Error: Library Coq.Program.Tactics has to be required first.

Indeed adding Require Coq.Program.Tactics. at the beginning of finmap.v solves the problem.

compilation error due to Notation "[ 'fset[' key ] E | x : A , y : B ]"

as noticed by @affeldt-aist as well in this comment, finmap.dev doesn't compile anymore with coq.dev and mathcomp.dev

See e.g. https://gitlab.com/math-comp/math-comp/-/jobs/463594590#L568 :

568 - File "./finmap.v", line 831, characters 0-154:
569 - Error: Notation "[ fset[ _ ] _ | _ : _ , _ : _ ]" is already defined
570 - at level 0 with arguments constr, constr at level 99, constr at level 99,
571 - constr at level 200, constr at level 99, constr
572 - while it is now required to be at level 0 with arguments constr, constr
573 - at level 99, constr at level 99, constr, constr at level 99, constr.

so this seems to come from the fact this notation is defined twice with incompatible levels:

finmap/finmap.v

Lines 690 to 693 in 48c1330

	Notation "[ 'fset[' key ] E | x : A , y : B ]" :=
	[fset[key] E | x : _ in {: A}, y : _ in {: B}]
	(at level 0, E, x at level 99, A at level 200, y at level 99,
	only parsing) : fset_scope.

finmap/finmap.v

Lines 831 to 833 in 48c1330

	Notation "[ 'fset[' key ] E | x : A , y : B ]" :=
	[fset[key] E | x in {: A}, y in {: B}]
	(at level 0, E, x, y at level 99, only parsing) : fset_scope.

Cc @CohenCyril

Bad notations interaction

The notation [`x] badly interact with the [] selector and the notation for the norm.

Order-preserving morphisms

Is there a plan to define order-preserving morphisms and some of their theory?

Duplicate lemmas

Lemmas fsetD_eq0 and fsetB_eq0 are duplicated.

Plain not distributive lattices

In file https://github.com/math-comp/finmap/blob/master/order.v:

latticeType == the type of distributive lattices

I.E.: all lattices are assumed to be distributive. There is a lot to say on non-distributive lattices. I'd love to have them.

Some finmap/multiset lemmas that might be useful

Hello,

Through an experimental formalization of well-foundedness of multiset ordering, I found the following finmap/multiset lemmas convenient. Some of them might also be useful for general use.

(Update: proofs are slightly simplified. Previously I didn't notice mset1D1.)

Section BigFSetExt.

Local Open Scope fset_scope.

Variable (R : Type) (idx : R) (op : Monoid.com_law idx).

Lemma big_fincl (T : choiceType) (A B : {fset T}) (AsubB : A `<=` B)
      (P : pred B) (F : B -> R) :
  \big[op/idx]_(a : A | P (fincl AsubB a)) F (fincl AsubB a) =
  \big[op/idx]_(b : B | P b && (val b \in A)) F b.
Proof.
  have [Aisfset0 | [d dinA]] := fset_0Vmem A.
  - rewrite !big_pred0 //= => [b | a]; first by rewrite Aisfset0 inE andbF.
    by have := valP a; rewrite [X in _ \in X]Aisfset0 inE.
  - rewrite (reindex (fincl AsubB)).
    + by apply: eq_bigl => /= a; rewrite (valP a) andbT.
    + exists (fun b : B => insubd [` dinA] (val b)) => /= [a _ | a].
      * by apply: val_inj; rewrite val_insubd (valP a).
      * rewrite inE => /andP [_ vainA]; apply: val_inj.
        by rewrite /= val_insubd vainA.
Qed.

End BigFSetExt.


Section BigMSet.
Variable (R : Type) (idx : R) (op : Monoid.law idx).

Lemma big_mset0 (T : choiceType) (P : pred _) (F : _ -> R) :
  \big[op/idx]_(i : @mset0 T | P i) F i = idx :> R.
Proof. by apply: big_pred0 => -[j hj]; have := hj; rewrite in_mset0. Qed.

End BigMSet.


Section MSetTheoryExt.

Local Open Scope fset_scope.
Local Open Scope mset_scope.
Local Open Scope nat_scope.

Context {K : choiceType}.
Implicit Types (a b c : K) (A B C : {mset K}).

Lemma msub1set A a : ([mset a] `<=` A) = (a \in A).
Proof.
  apply/msubsetP/idP; first by move/(_ a); rewrite msetnxx in_mset.
  by move=> ainA b; rewrite msetnE; case: eqP => // ->; rewrite -in_mset.
Qed.

Lemma msetDBA A B C : C `<=` B -> A `+` B `\` C = (A `+` B) `\` C.
Proof.
  by move=> /msubsetP CB; apply/msetP=> a; rewrite !msetE2 addnBA.
Qed.

Lemma mset_0Vmem A : (A = mset0) + {x : K | x \in A}.
Proof.
  have [/fsetP Aisfset0 | [a ainA]] := fset_0Vmem A; last by right; exists a.
  left; apply/msetP => a; rewrite mset0E; apply/mset_eq0P.
  by rewrite Aisfset0 inE.
Qed.

Definition msetsize A := \sum_(a : A) A (val a).

Lemma msetsize0 : msetsize mset0 = 0.
Proof. exact: big_mset0. Qed.

Lemma msetsize_eq0 A : (msetsize A == 0) = (A == mset0).
Proof.
  rewrite sum_nat_eq0.
  apply/forallP/eqP => /= [Ax | -> a]; last by have := valP a; rewrite in_msetE.
  apply/msetP => a; rewrite mset0E; apply/mset_eq0P/negP => ainA.
  by have := Ax [` ainA] => /=; rewrite mset_eq0 ainA.
Qed.

Lemma msetsize1D a A : msetsize (a +` A) = (msetsize A).+1.
Proof.
  pose ainaA := [` mset1D1 a A].
  rewrite /msetsize (bigD1 ainaA) //= mset1DE eqxx add1n addSn; congr S.
  rewrite [X in _ + X](_ : _ = \sum_(b : a +` A | (b != ainaA) && (val b \in A))
                                A (val b)); last first.
  - apply: eq_big => a0; last by rewrite -!val_eqE /= mset1DE => /negbTE ->.
    by have := valP a0; rewrite -!val_eqE /= in_msetE; case: (val a0 == a).
  - have AsubaA: (A `<=` a +` A)%fset
      by apply/fsubsetP => a0; rewrite in_msetE => ->; rewrite orbT.
    have [ainA | aninA] := boolP (a \in A).
    + rewrite (bigD1 [` ainA]) //=; congr addn.
      by rewrite -big_fincl /=; apply: eq_bigl => a0; rewrite -!val_eqE.
    + rewrite (mset_eq0P aninA) add0n -big_fincl /=; apply: eq_bigl => a0.
      by rewrite -val_eqE /=; apply: contraNneq aninA => <-; apply: valP.
Qed.

Lemma mset_ind P:
  P mset0 -> (forall a A, P A -> P (a +` A)) -> forall A, P A.
Proof.
  move=> base step A.
  elim: {A}(msetsize A) {-2}A (erefl (msetsize A)) => [|n IHn] A.
  - by move/eqP; rewrite msetsize_eq0 => /eqP ->.
  - have [-> | [a ainA]] := mset_0Vmem A; first by rewrite msetsize0.
    by rewrite -(msetB1K _ _ ainA) msetsize1D => -[] /IHn; apply: step.
Qed.

Lemma msubset_ind B P:
  P B -> (forall A a, B `<=` A -> P A -> P (a +` A)) ->
  forall A, B `<=` A -> P A.
Proof.
  move=> base step A.
  elim/mset_ind: {A}(A `\` B) {-2}A (erefl (A `\` B)) => [| a D IH] A.
  - move/eqP. rewrite msetB_eq0 => AsubB BsubA.
    by rewrite (_ : A = B) //; apply/eqP; rewrite eqEmsubset AsubB BsubA.
  - move=> AdiffB BsubA.
    have: a \in A by rewrite -(msetBDKC _ _ BsubA) AdiffB in_msetE mset1D1 orbT.
    move/msetB1K => <-.
    have BsubAa: B `<=` A `\ a.
    + rewrite -(msetBBK _ _ BsubA); apply: msetBS.
      by rewrite AdiffB msub1set mset1D1.
    + apply: step => //; apply: IH => //.
      by rewrite -(msetD1K a D) -AdiffB -!msetBDA [in LHS]msetDC.
Qed.

End MSetTheoryExt.

Please pick the version you prefer for Coq 8.16 in Coq Platform 2022.09

The Coq team released Coq 8.16+rc1 on June 01, 2022.
The corresponding Coq Platform release 2022.09 should be released before September 15, 2022.
It can be delayed in case of difficulties until October 15, 2022, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.16+rc1.

Coq Platform CI is currently testing opam package coq-mathcomp-finmap.1.5.2
from official repository https://coq.inria.fr/opam/released/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.1.5.2/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2022.09, please inform us as soon as possible and before August 31, 2022!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.16+rc1~2022.09~preview1 which already supports Coq version 8.16+rc1 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#274

Notation issues for `imfset`

The following script showcases some unfortunate notation behaviors (on the current coq.dev and finmap.dev)

From mathcomp Require Import all_ssreflect finmap.

Open Scope fset_scope.
 
Lemma fsetIsep (T : choiceType) (A B : {fset T}) : 
  A `&` B = [fset x in A | x \in B].

(* Goal: A `&` B = [fset (x : T) | x in A & x \in B] *)

rewrite /fsetI.

(* Goal: [fset x | x in A & x \in B] = [fset x | x in A & x \in B] *)

Fail reflexivity.

apply/fsetP => x; rewrite !inE.

(* Goal: (x \in A) && (x \in B) = (x \in mem_fin (fset_finpred A)) && (x \in B) *)

rewrite /=.

(* Goal:  (x \in A) && (x \in B) = (x \in [eta mem_seq (T:=T) A]) && (x \in B) *)

reflexivity.

Qed.

Add finmap to Coq's CI

I'm opening this issue to track the result of a recent discussion on Gitter.

Coq 8.11.1 release broke coq-mathcomp-finmap on opam and some other packages that depend on it: coq-mathcomp-multinomials, coq-coqeal, and coq-ceramist.

Adding finmap to Coq's CI will help prevent this. Although it requires that the maintainers are ready to communicate with the Coq dev team in a timely manner and accept occasional patches. See https://github.com/coq/coq/blob/master/dev/ci/README-users.md for more detail.

subtype in order/lattices

I'm afraid I might be not expert enough with canonical structure to finish my pull request #8. Here is what could possibly done

1 - Any subtype of a porder/order and their finite version is canonically ordered. Except correctly dealing with canonicals there is nearly nothing to do here. Example of application : 'I_n, tuple...
2 - define a notion of lattice_closed saying that sup and inf are compatible with a predicate
3 - this allows to define a notion of sublattice

For me 1 is a prerequisite to switch to finmap what I did in https://github.com/hivert/Coq-Combi.

remove bigenough dependency

The opam package for finmap introduces a dependency on bigenough, which is not actually needed to build finmap. Can we remove this dependency?

Update description

The github "Description" for finmap says "Finite sets, finite maps, multisets and order". It should maybe be "Finite sets, finite maps, and multisets" now that order is in MathComp.

Fset of a fintype

Hi,
Is there a reason that a {fset T} with T a fintype isn't considered a fintype ?

Please pick the version you prefer for Coq 8.14 in Coq Platform 2021.11

The Coq team released Coq 8.14+rc1 on September 17, 2021 and plans to release Coq 8.14.0 before October 31, 2021.
The corresponding Coq Platform release 2021.11 should be released before November 30, 2021.
It can be delayed in case of difficulties until January 31, 2022, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.14+rc1.

Coq Platform CI is currently testing opam package coq-mathcomp-finmap.1.5.1
from official repository https://coq.inria.fr/opam/released.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2021.11, please inform as as soon as possible and before November 15, 2021!

The working branch of Coq Platform, which already supports Coq version 8.14+rc1, can be found here https://github.com/coq/platform/tree/main.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#139