From 5406d8ed531b9a73566f197cafccad296e475b7a Mon Sep 17 00:00:00 2001
From: Eelis van der Weegen <eelis@eelis.net>
Date: Fri, 4 Jun 2010 15:01:22 +0200
Subject: [PATCH] Update to Coq 8.2pl1.

---
 README.html            |  4 +++-
 abstract.v             |  4 ++--
 flow.v                 |  1 +
 interval_abstraction.v |  3 ++-
 interval_spec.v        |  1 +
 square_abstraction.v   |  1 +
 util.v                 | 18 +++++++++---------
 7 files changed, 19 insertions(+), 13 deletions(-)

diff --git a/README.html b/README.html
index bcc70e7..336dd0d 100644
--- a/README.html
+++ b/README.html
@@ -11,7 +11,9 @@ <h1>Readme</h1>
     <hr/><h2>1. Prerequisites</h2>
 
     <ul>
-      <li><a href='http://coq.inria.fr/'>Coq</a> 8.2 (at the moment this precise version is required; newer versions will not work)</li>
+      <li><a href='http://coq.inria.fr/'>Coq</a> 8.2pl1</li>
+      <li><a href='http://coq.inria.fr/distrib/current/contribs/CoRN.html'>CoRN</a></li>
+      <li><a href='http://color.inria.fr/download-color.html'>CoLoR</a></li>
       <li><a href='http://www.scons.org/'>SCons</a> &ge; 0.98 (SCons is a modern make-replacement based on Python)</li>
     </ul>
 
diff --git a/abstract.v b/abstract.v
index f6173bd..33b982f 100644
--- a/abstract.v
+++ b/abstract.v
@@ -90,8 +90,8 @@ Section contents.
 
     Context `{Container (c.State chs) C} `{Container (State ap) D} (cs: C) (ss: D).
 
-    Definition CompleteCover: Prop := forall s, s ∈ cs -> forall r, s ∈ r -> r ∈ ss.
-    Definition SharedCover: Prop := forall s, s ∈ cs -> DN (exists r, s ∈ r /\ r ∈ ss).
+    Definition CompleteCover: Prop := forall s: c.State chs, s ∈ cs -> forall r: State ap, s ∈ r -> r ∈ ss.
+    Definition SharedCover: Prop := forall s: c.State chs, s ∈ cs -> DN (exists r: State ap, s ∈ r /\ r ∈ ss).
 
   End CoverRelandsuch.
 
diff --git a/flow.v b/flow.v
index 005d80c..cdd9d87 100644
--- a/flow.v
+++ b/flow.v
@@ -3,6 +3,7 @@ Require Import geometry.
 Require Import CRreal.
 Require Import CRexp.
 Require Import CRln.
+Require Import Morphisms.
 Set Implicit Arguments.
 Open Local Scope CR_scope.
 
diff --git a/interval_abstraction.v b/interval_abstraction.v
index 9796fcb..5a3beed 100644
--- a/interval_abstraction.v
+++ b/interval_abstraction.v
@@ -1,5 +1,6 @@
 Require Import util c_util stability.
 Require geometry abstract abstract_cont_trans_over.
+Require Import Morphisms.
 
 Set Implicit Arguments.
 
@@ -53,7 +54,7 @@ Section contents.
     apply Some.
     intros p [H0 H4] t [H1 H5].
     apply (strongly_increasing_inv_mild (X p)).
-    unfold compose.
+    unfold Basics.compose.
     rewrite flow.flow_zero.
     apply CRle_trans with ('q)...
     rewrite A...
diff --git a/interval_spec.v b/interval_spec.v
index cc5fe8f..ba73bbe 100644
--- a/interval_spec.v
+++ b/interval_spec.v
@@ -1,5 +1,6 @@
 Require geometry abstract.
 Require Import bnat util c_util stability.
+Require Import Morphisms.
 
 Set Implicit Arguments.
 
diff --git a/square_abstraction.v b/square_abstraction.v
index c67d730..03b00b9 100644
--- a/square_abstraction.v
+++ b/square_abstraction.v
@@ -1,5 +1,6 @@
 Require interval_abstraction square_flow_conditions concrete EquivDec.
 Require Import List util list_util c_util geometry monotonic_flow stability.
+Require Import Morphisms.
 
 Set Implicit Arguments.
 
diff --git a/util.v b/util.v
index 2505197..84af04e 100644
--- a/util.v
+++ b/util.v
@@ -4,6 +4,8 @@ Require Import List.
 Require Import Bool.
 Require Export Program.
 Require Import EquivDec.
+Require Import Relation_Definitions.
+Require Import Morphisms.
 
 Set Implicit Arguments.
 Open Local Scope R_scope.
@@ -153,14 +155,14 @@ Qed.
 Instance option_eq_dec `(Bdec: EquivDec.EqDec B eq): EquivDec.EqDec (option B) eq.
 Proof with auto.
   intros B e Bdec o o'.
-  unfold equiv.
+  unfold Equivalence.equiv.
   destruct o; destruct o'...
-      destruct (Bdec b b0).
-        unfold equiv in *.
-        subst...
-      right. intro. inversion H...
-    right. intro. discriminate.
-  right. intro. discriminate.
+    destruct (Bdec b b0).
+     unfold Equivalence.equiv in *.
+     subst...
+    right. intro. inversion H...
+   right. discriminate.
+  right. discriminate.
 Defined.
 
 Coercion opt_to_bool A (o: option A): bool :=
@@ -276,8 +278,6 @@ Program Coercion decision_overestimation (P: Prop) (d: decision P): overestimati
 Next Obligation. destruct d; firstorder. Qed.
   (* todo: rename, because we can do the same for underestimation *)
 
-Coercion decision_overestimation: decision >-> overestimation.
-
 Definition decider_to_overestimator `{ipt: IsPredicateType T} (P: T): decider P -> overestimator P.
   unfold decider, overestimator.
   intro.