Merge pull request #27 from coq-community/prepare-8.15-release

Prepare 8.15 release
coq-community · Jul 22, 2022 · 3cd92b9 · 3cd92b9
2 parents a15a21f + 0c26082
commit 3cd92b9
Show file tree

Hide file tree

Showing 6 changed files with 5 additions and 11 deletions.
diff --git a/.gitignore b/.gitignore
@@ -2,8 +2,8 @@ Makefile.coq
 Makefile.coq.conf
 execute_loops.ml
 execute_loops.mli
-insert-sort.ml
-insert-sort.mli
+insert_sort.ml
+insert_sort.mli
 pplus.ml
 pplus.mli
 .lia.cache

diff --git a/Makefile.coq.local b/Makefile.coq.local
@@ -0,0 +1,2 @@
+clean::
+	$(HIDE)rm -f execute_loops.ml execute_loops.mli insert_sort.ml insert_sort.mli pplus.ml pplus.mli
diff --git a/ch14_fundations_of_inductive_types/SRC/chap14.v b/ch14_fundations_of_inductive_types/SRC/chap14.v
@@ -322,8 +322,6 @@ Scheme ntree_ind2 :=
    Induction for ntree Sort Prop
  with nforest_ind2 :=
    Induction for nforest Sort Prop.
-Arguments ntree_ind2 A P P0 : rename.
-Arguments nforest_ind2 A P P0 : rename.
 
 Inductive occurs (A:Type)(a:A) : ntree A -> Prop :=
 | occurs_root : forall l, occurs A a (nnode A a l)

diff --git a/ch14_fundations_of_inductive_types/SRC/ltree_to_ntree.v b/ch14_fundations_of_inductive_types/SRC/ltree_to_ntree.v
@@ -13,8 +13,6 @@ Scheme
 ntree_ind2 := Induction for ntree Sort Prop
    with
    nforest_ind2 := Induction for nforest Sort Prop.
-Arguments ntree_ind2 A P P0 : rename.
-Arguments nforest_ind2 A P P0 : rename.
 
 Section correct_ltree_ind.
 Variables (A : Type) (P : ltree A ->  Prop) (Q : list (ltree A) ->  Prop).

diff --git a/ch1_overview/SRC/chap1.v b/ch1_overview/SRC/chap1.v
@@ -154,6 +154,4 @@ Definition sort :
     +  now apply insert_sorted. 
 Defined.
 
-Extraction "insert-sort" insert sort.
-
-
+Extraction "insert_sort" insert sort.
diff --git a/tutorial_inductive_co_inductive_types/SRC/RecTutorial.v b/tutorial_inductive_co_inductive_types/SRC/RecTutorial.v
@@ -671,8 +671,6 @@ End Principle_of_Induction.
 
 Scheme Even_induction := Minimality for even Sort Prop
 with   Odd_induction  := Minimality for odd  Sort Prop.
-Arguments Even_induction P P0 : rename.
-Arguments Odd_induction P P0 : rename.
 
 Theorem even_plus_four : forall n:nat, even n -> even (4+n).
 Proof.
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		clean::
		$(HIDE)rm -f execute_loops.ml execute_loops.mli insert_sort.ml insert_sort.mli pplus.ml pplus.mli