Compare revisions

7f11a0db · 7f11a0db · 7f11a0db · 7f11a0db · 7f11a0db · 7f11a0db
--- a/stdpp/telescopes.v
+++ b/stdpp/telescopes.v
--- a/stdpp/vector.v
+++ b/stdpp/vector.v
--- a/stdpp/well_founded.v
+++ b/stdpp/well_founded.v
--- a/stdpp/zmap.v
+++ b/stdpp/zmap.v
--- a/stdpp_bitvector/bitvector.v
+++ b/stdpp_bitvector/bitvector.v
+(** This file is maintained by Michael Sammler. *)
+From stdpp.bitvector Require Export definitions tactics.
+From stdpp Require Import options.
--- a/stdpp_unstable/bitvector.v
+++ b/stdpp_unstable/bitvector.v
--- a/stdpp_bitvector/dune
+++ b/stdpp_bitvector/dune
--- a/stdpp_unstable/bitvector_tactics.v
+++ b/stdpp_unstable/bitvector_tactics.v
--- a/stdpp_unstable/bitblast.v
+++ b/stdpp_unstable/bitblast.v
--- a/stdpp_unstable/dune
+++ b/stdpp_unstable/dune
--- a/test-normalizer.sed
+++ b/test-normalizer.sed
--- a/tests/ascii.ref
+++ b/tests/ascii.ref
--- a/tests/ascii.v
+++ b/tests/ascii.v
--- a/tests/bitvector.ref
+++ b/tests/bitvector.ref
--- a/tests/bitvector.v
+++ b/tests/bitvector.v
--- a/tests/bitvector_tactics.ref
+++ b/tests/bitvector_tactics.ref
--- a/tests/bitvector_tactics.v
+++ b/tests/bitvector_tactics.v
--- a/tests/decidable.ref
+++ b/tests/decidable.ref
--- a/tests/decidable.v
+++ b/tests/decidable.v
--- a/tests/fin.ref
+++ b/tests/fin.ref
No results found