Compatibility with coq 8.20.
coq 8.20 has a small regression with lia. + some small stdlib changes.
Showing
- CaseStudies/Convergence/Algorithm_noB.v 1 addition, 0 deletionsCaseStudies/Convergence/Algorithm_noB.v
- CaseStudies/Convergence/Impossibility_2G_1B.v 3 additions, 5 deletionsCaseStudies/Convergence/Impossibility_2G_1B.v
- CaseStudies/Gathering/Impossibility.v 4 additions, 3 deletionsCaseStudies/Gathering/Impossibility.v
- CaseStudies/Gathering/InR/Algorithm.v 43 additions, 27 deletionsCaseStudies/Gathering/InR/Algorithm.v
- CaseStudies/Gathering/InR/Impossibility.v 2 additions, 1 deletionCaseStudies/Gathering/InR/Impossibility.v
- CaseStudies/Gathering/InR2/Algorithm.v 1 addition, 1 deletionCaseStudies/Gathering/InR2/Algorithm.v
- CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v 1 addition, 0 deletionsCaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
- CaseStudies/Gathering/InR2/Peleg.v 1 addition, 0 deletionsCaseStudies/Gathering/InR2/Peleg.v
- CaseStudies/Gathering/WithMultiplicity.v 5 additions, 5 deletionsCaseStudies/Gathering/WithMultiplicity.v
- CaseStudies/LifeLine/Algorithm.v 3 additions, 3 deletionsCaseStudies/LifeLine/Algorithm.v
- Core/Formalism.v 2 additions, 1 deletionCore/Formalism.v
- Makefile.local 10 additions, 2 deletionsMakefile.local
- Models/GraphEquivalence.v 50 additions, 8 deletionsModels/GraphEquivalence.v
- Models/RigidFlexibleEquivalence.v 1 addition, 0 deletionsModels/RigidFlexibleEquivalence.v
- Observations/LimitedMultisetObservation.v 1 addition, 2 deletionsObservations/LimitedMultisetObservation.v
- Observations/LimitedSetObservation.v 2 additions, 2 deletionsObservations/LimitedSetObservation.v
- Spaces/Grid.v 18 additions, 17 deletionsSpaces/Grid.v
- Spaces/R2.v 1 addition, 1 deletionSpaces/R2.v
- Util/Bijection.v 11 additions, 11 deletionsUtil/Bijection.v
- Util/FMaps/FMapFacts.v 1 addition, 1 deletionUtil/FMaps/FMapFacts.v
Loading
Please register or sign in to comment