Some comments are triggering charlock binary

4 files changed, 22 insertions, 60 deletions

diff --git a/samples/Coq/Heap.v b/samples/Coq/Heap.v
index 8653640..4881c99 100755
--- a/samples/Coq/Heap.v
+++ b/samples/Coq/Heap.v
@@ -1,13 +1,3 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** This file is deprecated, for a tree on list, use [Mergesort.v]. *)
-
 (** A development of Treesort on Heap trees. It has an average
     complexity of O(n.log n) but of O(n²) in the worst case (e.g. if
     the list is already sorted) *)
@@ -88,9 +78,9 @@ Section defs.
     forall P:Tree -> Type,
       P Tree_Leaf ->
       (forall (a:A) (T1 T2:Tree),
-	leA_Tree a T1 ->
-	leA_Tree a T2 ->
-	is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
+        leA_Tree a T1 ->
+        leA_Tree a T2 ->
+        is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
       forall T:Tree, is_heap T -> P T.
   Proof.
     simple induction T; auto with datatypes.
@@ -105,9 +95,9 @@ Section defs.
     forall P:Tree -> Set,
       P Tree_Leaf ->
       (forall (a:A) (T1 T2:Tree),
-	leA_Tree a T1 ->
-	leA_Tree a T2 ->
-	is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
+        leA_Tree a T1 ->
+        leA_Tree a T2 ->
+        is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
       forall T:Tree, is_heap T -> P T.
   Proof.
     simple induction T; auto with datatypes.
@@ -135,13 +125,13 @@ Section defs.
       (forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) ->
       merge_lem l1 l2.
   Require Import Morphisms.
-  
+
   Instance: Equivalence (@meq A).
   Proof. constructor; auto with datatypes. red. apply meq_trans. Defined.
 
   Instance: Proper (@meq A ++> @meq _ ++> @meq _) (@munion A).
   Proof. intros x y H x' y' H'. now apply meq_congr. Qed.
-  
+
   Lemma merge :
     forall l1:list A, Sorted leA l1 ->
     forall l2:list A, Sorted leA l2 -> merge_lem l1 l2.
@@ -150,8 +140,8 @@ Section defs.
     apply merge_exist with l2; auto with datatypes.
     rename l1 into l.
     revert l2 H0. fix 1. intros.
-    destruct l2 as [|a0 l0]. 
-    apply merge_exist with (a :: l); simpl; auto with datatypes. 
+    destruct l2 as [|a0 l0].
+    apply merge_exist with (a :: l); simpl; auto with datatypes.
     elim (leA_dec a a0); intros.
 
     (* 1 (leA a a0) *)
@@ -159,18 +149,18 @@ Section defs.
     destruct (merge l H (a0 :: l0) H0).
     apply merge_exist with (a :: l1). clear merge merge0.
       auto using cons_sort, cons_leA with datatypes.
-    simpl. rewrite m. now rewrite munion_ass. 
-    intros. apply cons_leA. 
+    simpl. rewrite m. now rewrite munion_ass.
+    intros. apply cons_leA.
     apply (@HdRel_inv _ leA) with l; trivial with datatypes.
 
     (* 2 (leA a0 a) *)
     apply Sorted_inv in H0. destruct H0.
-    destruct (merge0 l0 H0). clear merge merge0.  
-    apply merge_exist with (a0 :: l1); 
+    destruct (merge0 l0 H0). clear merge merge0.
+    apply merge_exist with (a0 :: l1);
       auto using cons_sort, cons_leA with datatypes.
     simpl; rewrite m. simpl. setoid_rewrite munion_ass at 1. rewrite munion_comm.
     repeat rewrite munion_ass. setoid_rewrite munion_comm at 3. reflexivity.
-    intros. apply cons_leA. 
+    intros. apply cons_leA.
     apply (@HdRel_inv _ leA) with l0; trivial with datatypes.
   Qed.
 
@@ -186,7 +176,7 @@ Section defs.
     match t with
       | Tree_Leaf => emptyBag
       | Tree_Node a t1 t2 =>
-	munion (contents t1) (munion (contents t2) (singletonBag a))
+        munion (contents t1) (munion (contents t2) (singletonBag a))
     end.
 
 
@@ -272,11 +262,11 @@ Section defs.
     apply flat_exist with (a :: l); simpl; auto with datatypes.
     apply meq_trans with
       (munion (list_contents _ eqA_dec l1)
-	(munion (list_contents _ eqA_dec l2) (singletonBag a))).
+        (munion (list_contents _ eqA_dec l2) (singletonBag a))).
     apply meq_congr; auto with datatypes.
     apply meq_trans with
       (munion (singletonBag a)
-	(munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2))).
+        (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2))).
     apply munion_rotate.
     apply meq_right; apply meq_sym; trivial with datatypes.
   Qed.
diff --git a/samples/Coq/PermutSetoid.v b/samples/Coq/PermutSetoid.v
index aed7150..2e0dd17 100755
--- a/samples/Coq/PermutSetoid.v
+++ b/samples/Coq/PermutSetoid.v
@@ -1,11 +1,3 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
 Require Import Omega Relations Multiset SetoidList.
 
 (** This file is deprecated, use [Permutation.v] instead.
@@ -154,7 +146,7 @@ Lemma permut_add_cons_inside :
 Proof.
   intros;
     replace (a :: l) with ([] ++ a :: l); trivial;
-	apply permut_add_inside; trivial.
+        apply permut_add_inside; trivial.
 Qed.
 
 Lemma permut_middle :
@@ -168,8 +160,8 @@ Lemma permut_sym_app :
 Proof.
   intros l1 l2;
     unfold permutation, meq;
-	intro a; do 2 rewrite list_contents_app; simpl;
-	  auto with arith.
+        intro a; do 2 rewrite list_contents_app; simpl;
+          auto with arith.
 Qed.
 
 Lemma permut_rev :
diff --git a/samples/Coq/Permutation.v b/samples/Coq/Permutation.v
index eb769b7..4761fb6 100755
--- a/samples/Coq/Permutation.v
+++ b/samples/Coq/Permutation.v
@@ -1,17 +1,5 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*********************************************************************)
-(** * List permutations as a composition of adjacent transpositions  *)
-(*********************************************************************)
-
 (* Adapted in May 2006 by Jean-Marc Notin from initial contents by
-   Laurent Théry (Huffmann contribution, October 2003) *)
+   Laurent Thery (Huffmann contribution, October 2003) *)
 
 Require Import List Setoid Compare_dec Morphisms.
 Import ListNotations. (* For notations [] and [a;b;c] *)
diff --git a/samples/Coq/Sorting.v b/samples/Coq/Sorting.v
index 22e5659..edb10c6 100755
--- a/samples/Coq/Sorting.v
+++ b/samples/Coq/Sorting.v
@@ -1,10 +1,2 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
 Require Export Sorted.
 Require Export Mergesort.