Update to Coq 8.2pl1.

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>
 

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.
 

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.
 

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...

interval_spec.v

@@ -1,5 +1,6 @@
 Require geometry abstract.
 Require Import bnat util c_util stability.
+Require Import Morphisms.
 
 Set Implicit Arguments.
 

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.
 

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.