reorganize to work on Coq 8.9.1 with ssreflect 1.7.0

coq-community · Sep 8, 2020 · 80413dc · 80413dc
1 parent a643d47
commit 80413dc
Show file tree

Hide file tree

Showing 45 changed files with 72 additions and 50 deletions.
diff --git a/.gitignore 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
@@ -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
@@ -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 → theories/fibm.v b/fibm.v → theories/fibm.v
diff --git a/sset1.v → theories/sset1.v b/sset1.v → theories/sset1.v
diff --git a/sset10.v → theories/sset10.v b/sset10.v → theories/sset10.v
diff --git a/sset11.v → theories/sset11.v b/sset11.v → theories/sset11.v
diff --git a/sset12.v → theories/sset12.v b/sset12.v → theories/sset12.v
diff --git a/sset13a.v → theories/sset13a.v b/sset13a.v → theories/sset13a.v
diff --git a/sset13b.v → theories/sset13b.v b/sset13b.v → theories/sset13b.v
diff --git a/sset13c.v → theories/sset13c.v b/sset13c.v → theories/sset13c.v
diff --git a/sset14.v → theories/sset14.v b/sset14.v → theories/sset14.v
diff --git a/sset15.v → theories/sset15.v b/sset15.v → theories/sset15.v
diff --git a/sset16a.v → theories/sset16a.v b/sset16a.v → theories/sset16a.v
diff --git a/sset16b.v → theories/sset16b.v b/sset16b.v → theories/sset16b.v
diff --git a/sset16c.v → theories/sset16c.v b/sset16c.v → theories/sset16c.v
diff --git a/sset17.v → theories/sset17.v b/sset17.v → theories/sset17.v
diff --git a/sset18.v → theories/sset18.v b/sset18.v → theories/sset18.v
diff --git a/sset19.v → theories/sset19.v b/sset19.v → theories/sset19.v
diff --git a/sset2.v → theories/sset2.v b/sset2.v → theories/sset2.v
diff --git a/sset2_aux.v → theories/sset2_aux.v b/sset2_aux.v → theories/sset2_aux.v
diff --git a/sset3.v → theories/sset3.v b/sset3.v → theories/sset3.v
diff --git a/sset4.v → theories/sset4.v b/sset4.v → theories/sset4.v
diff --git a/sset5.v → theories/sset5.v b/sset5.v → theories/sset5.v
diff --git a/sset6.v → theories/sset6.v b/sset6.v → theories/sset6.v
diff --git a/sset7.v → theories/sset7.v b/sset7.v → theories/sset7.v
diff --git a/sset8.v → theories/sset8.v b/sset8.v → theories/sset8.v
diff --git a/sset9.v → theories/sset9.v b/sset9.v → theories/sset9.v
diff --git a/ssetc.v → theories/ssetc.v b/ssetc.v → theories/ssetc.v
diff --git a/ssete1.v → theories/ssete1.v b/ssete1.v → theories/ssete1.v
diff --git a/ssete10.v → theories/ssete10.v b/ssete10.v → theories/ssete10.v
diff --git a/ssete11.v → theories/ssete11.v b/ssete11.v → theories/ssete11.v
diff --git a/ssete2.v → theories/ssete2.v b/ssete2.v → theories/ssete2.v
diff --git a/ssete3.v → theories/ssete3.v b/ssete3.v → theories/ssete3.v
diff --git a/ssete4.v → theories/ssete4.v b/ssete4.v → theories/ssete4.v
diff --git a/ssete5.v → theories/ssete5.v b/ssete5.v → theories/ssete5.v
diff --git a/ssete6.v → theories/ssete6.v b/ssete6.v → theories/ssete6.v
diff --git a/ssete7.v → theories/ssete7.v b/ssete7.v → theories/ssete7.v
diff --git a/ssete8.v → theories/ssete8.v b/ssete8.v → theories/ssete8.v
diff --git a/ssete9.v → theories/ssete9.v b/ssete9.v → theories/ssete9.v
diff --git a/ssetq1.v → theories/ssetq1.v b/ssetq1.v → theories/ssetq1.v
diff --git a/ssetq2.v → theories/ssetq2.v b/ssetq2.v → theories/ssetq2.v
diff --git a/ssetr.v → theories/ssetr.v b/ssetr.v → theories/ssetr.v
diff --git a/ssetz.v → theories/ssetz.v b/ssetz.v → theories/ssetz.v
diff --git a/stern.v → theories/stern.v b/stern.v → 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.
-
-
-
-
-