Compare revisions

9274984b · 9274984b · 9274984b · 9274984b · 9274984b · 9274984b
--- a/theories/proof_irrel.v
+++ b/theories/proof_irrel.v
--- a/theories/propset.v
+++ b/theories/propset.v
--- a/theories/relations.v
+++ b/theories/relations.v
--- a/theories/sets.v
+++ b/theories/sets.v
--- a/theories/sorting.v
+++ b/theories/sorting.v
--- a/stdpp/ssreflect.v
+++ b/stdpp/ssreflect.v
--- a/theories/streams.v
+++ b/theories/streams.v
--- a/theories/stringmap.v
+++ b/theories/stringmap.v
--- a/stdpp/strings.v
+++ b/stdpp/strings.v
--- a/theories/tactics.v
+++ b/theories/tactics.v
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
--- a/theories/vector.v
+++ b/theories/vector.v
--- a/stdpp/well_founded.v
+++ b/stdpp/well_founded.v
--- a/theories/zmap.v
+++ b/theories/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_bitvector/definitions.v
+++ b/stdpp_bitvector/definitions.v
--- a/stdpp_bitvector/dune
+++ b/stdpp_bitvector/dune
+(include_subdirs qualified)
+(coq.theory
+ (name stdpp.bitvector)
+ (package coq-stdpp-bitvector)
+ (theories stdpp))
--- a/stdpp_bitvector/tactics.v
+++ b/stdpp_bitvector/tactics.v
--- a/stdpp_unstable/bitblast.v
+++ b/stdpp_unstable/bitblast.v
--- a/stdpp_unstable/dune
+++ b/stdpp_unstable/dune
No results found