From 80413dc7d7747a602793107632fefac73d79aa43 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Tue, 8 Sep 2020 06:43:10 -0500
Subject: [PATCH] reorganize to work on Coq 8.9.1 with ssreflect 1.7.0

---
 .gitignore                          | 11 ++++
 Makefile                            | 16 ++++++
 _CoqProject                         | 86 ++++++++++++++---------------
 fibm.v => theories/fibm.v           |  0
 sset1.v => theories/sset1.v         |  0
 sset10.v => theories/sset10.v       |  0
 sset11.v => theories/sset11.v       |  0
 sset12.v => theories/sset12.v       |  0
 sset13a.v => theories/sset13a.v     |  0
 sset13b.v => theories/sset13b.v     |  0
 sset13c.v => theories/sset13c.v     |  0
 sset14.v => theories/sset14.v       |  0
 sset15.v => theories/sset15.v       |  0
 sset16a.v => theories/sset16a.v     |  0
 sset16b.v => theories/sset16b.v     |  0
 sset16c.v => theories/sset16c.v     |  0
 sset17.v => theories/sset17.v       |  0
 sset18.v => theories/sset18.v       |  0
 sset19.v => theories/sset19.v       |  0
 sset2.v => theories/sset2.v         |  0
 sset2_aux.v => theories/sset2_aux.v |  0
 sset3.v => theories/sset3.v         |  0
 sset4.v => theories/sset4.v         |  0
 sset5.v => theories/sset5.v         |  0
 sset6.v => theories/sset6.v         |  0
 sset7.v => theories/sset7.v         |  0
 sset8.v => theories/sset8.v         |  0
 sset9.v => theories/sset9.v         |  0
 ssetc.v => theories/ssetc.v         |  0
 ssete1.v => theories/ssete1.v       |  0
 ssete10.v => theories/ssete10.v     |  0
 ssete11.v => theories/ssete11.v     |  0
 ssete2.v => theories/ssete2.v       |  0
 ssete3.v => theories/ssete3.v       |  0
 ssete4.v => theories/ssete4.v       |  0
 ssete5.v => theories/ssete5.v       |  0
 ssete6.v => theories/ssete6.v       |  0
 ssete7.v => theories/ssete7.v       |  0
 ssete8.v => theories/ssete8.v       |  0
 ssete9.v => theories/ssete9.v       |  0
 ssetq1.v => theories/ssetq1.v       |  0
 ssetq2.v => theories/ssetq2.v       |  0
 ssetr.v => theories/ssetr.v         |  0
 ssetz.v => theories/ssetz.v         |  0
 stern.v => theories/stern.v         |  9 +--
 45 files changed, 72 insertions(+), 50 deletions(-)
 create mode 100644 .gitignore
 create mode 100644 Makefile
 rename fibm.v => theories/fibm.v (100%)
 rename sset1.v => theories/sset1.v (100%)
 rename sset10.v => theories/sset10.v (100%)
 rename sset11.v => theories/sset11.v (100%)
 rename sset12.v => theories/sset12.v (100%)
 rename sset13a.v => theories/sset13a.v (100%)
 rename sset13b.v => theories/sset13b.v (100%)
 rename sset13c.v => theories/sset13c.v (100%)
 rename sset14.v => theories/sset14.v (100%)
 rename sset15.v => theories/sset15.v (100%)
 rename sset16a.v => theories/sset16a.v (100%)
 rename sset16b.v => theories/sset16b.v (100%)
 rename sset16c.v => theories/sset16c.v (100%)
 rename sset17.v => theories/sset17.v (100%)
 rename sset18.v => theories/sset18.v (100%)
 rename sset19.v => theories/sset19.v (100%)
 rename sset2.v => theories/sset2.v (100%)
 rename sset2_aux.v => theories/sset2_aux.v (100%)
 rename sset3.v => theories/sset3.v (100%)
 rename sset4.v => theories/sset4.v (100%)
 rename sset5.v => theories/sset5.v (100%)
 rename sset6.v => theories/sset6.v (100%)
 rename sset7.v => theories/sset7.v (100%)
 rename sset8.v => theories/sset8.v (100%)
 rename sset9.v => theories/sset9.v (100%)
 rename ssetc.v => theories/ssetc.v (100%)
 rename ssete1.v => theories/ssete1.v (100%)
 rename ssete10.v => theories/ssete10.v (100%)
 rename ssete11.v => theories/ssete11.v (100%)
 rename ssete2.v => theories/ssete2.v (100%)
 rename ssete3.v => theories/ssete3.v (100%)
 rename ssete4.v => theories/ssete4.v (100%)
 rename ssete5.v => theories/ssete5.v (100%)
 rename ssete6.v => theories/ssete6.v (100%)
 rename ssete7.v => theories/ssete7.v (100%)
 rename ssete8.v => theories/ssete8.v (100%)
 rename ssete9.v => theories/ssete9.v (100%)
 rename ssetq1.v => theories/ssetq1.v (100%)
 rename ssetq2.v => theories/ssetq2.v (100%)
 rename ssetr.v => theories/ssetr.v (100%)
 rename ssetz.v => theories/ssetz.v (100%)
 rename stern.v => theories/stern.v (99%)

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..d1c60ad
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,11 @@
+Makefile.coq
+Makefile.coq.conf
+_build
+*~
+*.d
+*.aux
+*.glob
+*.vo
+*.vio
+*.vok
+*.vos
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..ad909e5
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,16 @@
+all: Makefile.coq
+	@+$(MAKE) -f Makefile.coq all
+
+clean: Makefile.coq
+	@+$(MAKE) -f Makefile.coq cleanall
+	@rm -f Makefile.coq Makefile.coq.conf
+
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
+
+force _CoqProject Makefile: ;
+
+%: Makefile.coq force
+	@+$(MAKE) -f Makefile.coq $@
+
+.PHONY: all clean force
diff --git a/_CoqProject b/_CoqProject
index 56f0f31..21d9483 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,43 +1,43 @@
--R . bourbaki
-fibm.v
-sset1.v
-sset10.v
-sset11.v
-sset12.v
-sset13a.v
-sset13b.v
-sset13c.v
-sset14.v
-sset15.v
-sset16a.v
-sset16b.v
-sset16c.v
-sset17.v
-sset18.v
-sset19.v
-sset2.v
-sset2_aux.v
-sset3.v
-sset4.v
-sset5.v
-sset6.v
-sset7.v
-sset8.v
-sset9.v
-ssetc.v
-ssete1.v
-ssete10.v
-ssete11.v
-ssete2.v
-ssete3.v
-ssete4.v
-ssete5.v
-ssete6.v
-ssete7.v
-ssete8.v
-ssete9.v
-ssetq1.v
-ssetq2.v
-ssetr.v
-ssetz.v
-stern.v
+-R theories gaia
+theories/fibm.v
+theories/sset1.v
+theories/sset10.v
+theories/sset11.v
+theories/sset12.v
+theories/sset13a.v
+theories/sset13b.v
+theories/sset13c.v
+theories/sset14.v
+theories/sset15.v
+theories/sset16a.v
+theories/sset16b.v
+theories/sset16c.v
+theories/sset17.v
+theories/sset18.v
+theories/sset19.v
+theories/sset2.v
+theories/sset2_aux.v
+theories/sset3.v
+theories/sset4.v
+theories/sset5.v
+theories/sset6.v
+theories/sset7.v
+theories/sset8.v
+theories/sset9.v
+theories/ssetc.v
+theories/ssete1.v
+theories/ssete10.v
+theories/ssete11.v
+theories/ssete2.v
+theories/ssete3.v
+theories/ssete4.v
+theories/ssete5.v
+theories/ssete6.v
+theories/ssete7.v
+theories/ssete8.v
+theories/ssete9.v
+theories/ssetq1.v
+theories/ssetq2.v
+theories/ssetr.v
+theories/ssetz.v
+theories/stern.v
diff --git a/fibm.v b/theories/fibm.v
similarity index 100%
rename from fibm.v
rename to theories/fibm.v
diff --git a/sset1.v b/theories/sset1.v
similarity index 100%
rename from sset1.v
rename to theories/sset1.v
diff --git a/sset10.v b/theories/sset10.v
similarity index 100%
rename from sset10.v
rename to theories/sset10.v
diff --git a/sset11.v b/theories/sset11.v
similarity index 100%
rename from sset11.v
rename to theories/sset11.v
diff --git a/sset12.v b/theories/sset12.v
similarity index 100%
rename from sset12.v
rename to theories/sset12.v
diff --git a/sset13a.v b/theories/sset13a.v
similarity index 100%
rename from sset13a.v
rename to theories/sset13a.v
diff --git a/sset13b.v b/theories/sset13b.v
similarity index 100%
rename from sset13b.v
rename to theories/sset13b.v
diff --git a/sset13c.v b/theories/sset13c.v
similarity index 100%
rename from sset13c.v
rename to theories/sset13c.v
diff --git a/sset14.v b/theories/sset14.v
similarity index 100%
rename from sset14.v
rename to theories/sset14.v
diff --git a/sset15.v b/theories/sset15.v
similarity index 100%
rename from sset15.v
rename to theories/sset15.v
diff --git a/sset16a.v b/theories/sset16a.v
similarity index 100%
rename from sset16a.v
rename to theories/sset16a.v
diff --git a/sset16b.v b/theories/sset16b.v
similarity index 100%
rename from sset16b.v
rename to theories/sset16b.v
diff --git a/sset16c.v b/theories/sset16c.v
similarity index 100%
rename from sset16c.v
rename to theories/sset16c.v
diff --git a/sset17.v b/theories/sset17.v
similarity index 100%
rename from sset17.v
rename to theories/sset17.v
diff --git a/sset18.v b/theories/sset18.v
similarity index 100%
rename from sset18.v
rename to theories/sset18.v
diff --git a/sset19.v b/theories/sset19.v
similarity index 100%
rename from sset19.v
rename to theories/sset19.v
diff --git a/sset2.v b/theories/sset2.v
similarity index 100%
rename from sset2.v
rename to theories/sset2.v
diff --git a/sset2_aux.v b/theories/sset2_aux.v
similarity index 100%
rename from sset2_aux.v
rename to theories/sset2_aux.v
diff --git a/sset3.v b/theories/sset3.v
similarity index 100%
rename from sset3.v
rename to theories/sset3.v
diff --git a/sset4.v b/theories/sset4.v
similarity index 100%
rename from sset4.v
rename to theories/sset4.v
diff --git a/sset5.v b/theories/sset5.v
similarity index 100%
rename from sset5.v
rename to theories/sset5.v
diff --git a/sset6.v b/theories/sset6.v
similarity index 100%
rename from sset6.v
rename to theories/sset6.v
diff --git a/sset7.v b/theories/sset7.v
similarity index 100%
rename from sset7.v
rename to theories/sset7.v
diff --git a/sset8.v b/theories/sset8.v
similarity index 100%
rename from sset8.v
rename to theories/sset8.v
diff --git a/sset9.v b/theories/sset9.v
similarity index 100%
rename from sset9.v
rename to theories/sset9.v
diff --git a/ssetc.v b/theories/ssetc.v
similarity index 100%
rename from ssetc.v
rename to theories/ssetc.v
diff --git a/ssete1.v b/theories/ssete1.v
similarity index 100%
rename from ssete1.v
rename to theories/ssete1.v
diff --git a/ssete10.v b/theories/ssete10.v
similarity index 100%
rename from ssete10.v
rename to theories/ssete10.v
diff --git a/ssete11.v b/theories/ssete11.v
similarity index 100%
rename from ssete11.v
rename to theories/ssete11.v
diff --git a/ssete2.v b/theories/ssete2.v
similarity index 100%
rename from ssete2.v
rename to theories/ssete2.v
diff --git a/ssete3.v b/theories/ssete3.v
similarity index 100%
rename from ssete3.v
rename to theories/ssete3.v
diff --git a/ssete4.v b/theories/ssete4.v
similarity index 100%
rename from ssete4.v
rename to theories/ssete4.v
diff --git a/ssete5.v b/theories/ssete5.v
similarity index 100%
rename from ssete5.v
rename to theories/ssete5.v
diff --git a/ssete6.v b/theories/ssete6.v
similarity index 100%
rename from ssete6.v
rename to theories/ssete6.v
diff --git a/ssete7.v b/theories/ssete7.v
similarity index 100%
rename from ssete7.v
rename to theories/ssete7.v
diff --git a/ssete8.v b/theories/ssete8.v
similarity index 100%
rename from ssete8.v
rename to theories/ssete8.v
diff --git a/ssete9.v b/theories/ssete9.v
similarity index 100%
rename from ssete9.v
rename to theories/ssete9.v
diff --git a/ssetq1.v b/theories/ssetq1.v
similarity index 100%
rename from ssetq1.v
rename to theories/ssetq1.v
diff --git a/ssetq2.v b/theories/ssetq2.v
similarity index 100%
rename from ssetq2.v
rename to theories/ssetq2.v
diff --git a/ssetr.v b/theories/ssetr.v
similarity index 100%
rename from ssetr.v
rename to theories/ssetr.v
diff --git a/ssetz.v b/theories/ssetz.v
similarity index 100%
rename from ssetz.v
rename to theories/ssetz.v
diff --git a/stern.v b/theories/stern.v
similarity index 99%
rename from stern.v
rename to theories/stern.v
index e84eda2..f5e7ba4 100644
--- a/stern.v
+++ b/theories/stern.v
@@ -156,10 +156,10 @@ Fixpoint pos_of_list l :=
 end.
 
 Definition num_of_list l :=
-  if l is a :: b then Npos (pos_of_list l) else 0%num.
+  if l is a :: b then Npos (pos_of_list l) else N0.
 
 Lemma list_of_posK: cancel list_of_pos pos_of_list.
-Proof. by elim => // p /= -> ;case: p. Qed. 
+Proof. by elim => // p /= -> ;case: p. Qed.
 
 Lemma list_of_numK: cancel list_of_num num_of_list.
 Proof. by case => // p /=; rewrite -{2} (list_of_posK p);case: p. Qed.
@@ -4982,8 +4982,3 @@ Abort.
 
 (* ----- *)
 End Stern.
-
-
-
-
-