more changes for 8.5 compatibility

lib/ModuRes/BI.v

@@ -673,7 +673,7 @@ Section MonotoneLater.
   Qed.
 
   Global Program Instance later_mon_morph : Later (U -m> T) :=
-    Build_Later _ _ _ _ _ _ _ m[(fun f => m[(fun u => later (f u))])] _ _ _.
+    Build_Later _ _ _ _ _ _ _ m[(fun f: U -m> T => m[(fun u => later (f u))])] _ _ _.
   Next Obligation.
     intros u; simpl morph; apply later_mon.
   Qed.
@@ -695,7 +695,7 @@ Section MComplUP.
     Context T `{pcmT : pcmType T} {eT : extensible T}.
 
     Program Definition mclose_up : (T -n> UPred V) -n> T -m> UPred V :=
-      n[(fun f => m[(fun t => mkUPred (fun n v => forall t', t ⊑ t' -> f t' n v) _)])].
+      n[(fun f: T -n> UPred V => m[(fun t => mkUPred (fun n v => forall t', t ⊑ t' -> f t' n v) _)])].
     Next Obligation.
       intros n m v1 v2 HLe HSubv HT t' HSubt.
       rewrite HLe, <- HSubv; apply HT, HSubt.
@@ -744,7 +744,7 @@ End MComplUP.
     Context U `{pcmU : pcmType U} {eU : extensible U}.
 
     Program Definition mclose_mm : (U -n> V -m> B) -n> U -m> V -m> B :=
-      n[(fun f => mcurry (mclose n[(fun uv => f (fst uv) (snd uv))]))].
+      n[(fun f:U -n> V -m> B  => mcurry (mclose n[(fun uv => f (fst uv) (snd uv))]))].
     Next Obligation.
       intros [u1 v1] [u2 v2] [EQu EQv]; simpl morph.
       unfold fst, snd in *; rewrite EQu, EQv; reflexivity.

lib/ModuRes/CBUltInst.v

@@ -67,7 +67,7 @@ Section Halving_Fun.
   Definition HF := fun T1 T2 => halveCM (F T1 T2).
 
   Program Instance halveFMap : BiFMap HF :=
-    fun m1 m2 m3 m4 => lift2m (lift2s (fun (ars: (m2 -t> m1) * (m3 -t> m4)) (ob: halveCM (F m1 m3)) => halvedT (fmorph (F := F) ars (unhalvedT ob))) _ _) _ _.
+    fun m1 m2 m3 m4 => lift2m (lift2s (fun (ars: (m2 -t> m1) * (m3 -t> m4)) (ob: halveCM (F m1 m3)) => halvedT (fmorph (F := F) (BiFMap := FA) ars (unhalvedT ob))) _ _) _ _.
   Next Obligation.
     repeat intro. unfold halvedT, unhalvedT, HF in *. simpl.
     unhalveT. simpl. rewrite H. reflexivity.
@@ -91,10 +91,10 @@ Section Halving_Fun.
     split; intros.
     + intros T; simpl.
       unfold unhalvedT, HF in *. unhalveT. simpl.
-      apply (fmorph_comp _ _ _ _ _ _ _ _ _ _ T).
+      apply (fmorph_comp (BiFunctor := FFun) _ _ _ _ _ _ _ _ _ _ T).
     + intros T; simpl.
       unfold unhalvedT, HF in *. unhalveT. simpl.
-      apply (fmorph_id _ _ T).
+      apply (fmorph_id (BiFunctor := FFun) _ _ T).
   Qed.
 
   Instance halve_contractive {m0 m1 m2 m3} :
@@ -102,7 +102,7 @@ Section Halving_Fun.
   Proof.
     intros n p1 p2 EQ f; simpl.
     unfold unhalvedT, HF in *. unhalveT. simpl.
-    change ((fmorph (F := F) p1) f = n = (fmorph p2) f).
+    change ((fmorph (F := F) (BiFMap := FA) p1) f = n = (fmorph (BiFMap := FA) p2) f).
     rewrite EQ; reflexivity.
   Qed.
 

lib/ModuRes/CSetoid.v

@@ -21,6 +21,15 @@ Qed.
 
 Notation "'mkType' R" := (@Build_Setoid _ R _) (at level 10).
 
+Ltac find_rewrite1 t0 t1 := match goal with
+                            | H: t0 = t1 |- _ => rewrite-> H
+                            | H: t0 == t1 |- _ => rewrite-> H
+                            | H: t1 = t0 |- _ => rewrite<- H
+                            | H: t1 == t0 |- _ => rewrite<- H
+                            end.
+Ltac find_rewrite2 t0 t1 t2 := find_rewrite1 t0 t1; find_rewrite1 t1 t2.
+Ltac find_rewrite3 t0 t1 t2 t3 := find_rewrite2 t0 t1 t2; find_rewrite1 t2 t3.
+
 (** A morphism between two types is an actual function together with a
     proof that it preserves equality. *)
 Record morphism S T `{eqS : Setoid S} `{eqT : Setoid T} :=
@@ -349,7 +358,7 @@ Section OptDefs.
     end.
 
   Program Definition moptbind : (T -=> option U) -=> option T -=> option U :=
-    lift2s optbind _ _.
+    lift2s (T:=T-=>option U) optbind _ _.
   Next Obligation.
     intros [v1 |] [v2 |] EQv; try (contradiction EQv || exact I); [].
     unfold optbind; apply x, EQv.
@@ -378,7 +387,7 @@ Section DiscreteType.
 End DiscreteType.
 
 Section ViewLemmas.
-  Require Import ssreflect.  
+  Require Import Ssreflect.ssreflect.  
   Context {T} `{eqT : Setoid T}.
   Implicit Types (t : T).
 

lib/ModuRes/CatBasics.v

 (** This module provides the basics to do category theory on metric spaces:
     Bundled types, indexed products on bundled types, and some functors. *)
 
-Require Import ssreflect.
+Require Import Ssreflect.ssreflect.
 Require Import Arith Min Max.
 Require Import MetricCore PreoMet.
 Require Fin.

lib/ModuRes/MetricRec.v

 Require Import MetricCore CatBasics.
-Require Import Arith.
+Require Import Arith Omega.
 
 (** A category enriched in complete bisected metric spaces and with a terminal object. *)
 
@@ -602,7 +602,7 @@ Module Solution(Cat : MCat)(M_cat : InputType(Cat)) : SolutionType(Cat)(M_cat).
         unfold binaryLimit, chainPE; simpl.
         rewrite 3!tcomp_assoc, <- (tcomp_assoc (Embeddings i ∘ Projection i)).
         simpl; rewrite fmorph_comp.
-        rewrite 2!retract_EP, fmorph_id, tid_right, <- (tcomp_assoc (Embeddings i)).
+        rewrite !retract_EP, fmorph_id, tid_right, <- (tcomp_assoc (Embeddings i)).
         rewrite retract_IP, tid_right; reflexivity.
       + symmetry; apply (colim_unique _ DCoLimit DCoLimit); intros n; rewrite tid_left; reflexivity.
     Qed.

lib/ModuRes/Predom.v

-Require Import ssreflect.
+Require Import Ssreflect.ssreflect.
 Require Export CSetoid.
 
 Generalizable Variables T U V W.

lib/ModuRes/PreoMet.v

-Require Import ssreflect.
+Require Import Ssreflect.ssreflect Omega.
 Require Export Predom MetricCore.
 
 Generalizable Variables T U V W X Y.

lib/ModuRes/RA.v

 (** Resource algebras: Commutative monoids with a validity predicate. *)
 
-Require Import ssreflect.
+Require Import Ssreflect.ssreflect.
 Require Import Coq.Classes.RelationPairs.
 Require Import Bool.
 Require Import Predom.
@@ -314,7 +314,12 @@ Section Id.
   Context {T} `{raT : RA T}.
 
   Program Definition raid : T -ra> T := ra[(mid T)].
-  Solve Obligations using reflexivity.
+  Next Obligation.
+    reflexivity.
+  Qed.
+  Next Obligation.
+    reflexivity.
+  Qed.
 End Id.
 
 Section Const.
@@ -476,7 +481,12 @@ Section Subra.
 
   (* The inclusion is an RA-morphism. *)
   Program Definition raincl : sub -ra> T := ra[(mincl)].
-  Solve Obligations using reflexivity.
+  Next Obligation.
+    reflexivity.
+  Qed.
+  Next Obligation.
+    reflexivity.
+  Qed.
 
   (* The inclusion is monic. *)
   Context {U} `{raU : RA U}.

lib/ModuRes/RAConstr.v

-Require Import ssreflect.
+Require Import Ssreflect.ssreflect Omega.
 Require Import PreoMet RA.
 
 Local Open Scope ra_scope.
@@ -282,11 +282,13 @@ Section DecAgreement.
       destruct (eq_dec t2 t0), (eq_dec t1 t); simpl; auto; exfalso;
       [ rewrite <- H, -> e in c | rewrite -> H, -> e in c; symmetry in c]; contradiction.
     - repeat (match goal with [ x : ra_dagree |- _ ] => destruct x end);
-      simpl in *; auto; try reflexivity; compute; try destruct (eq_dec _ _); try reflexivity.
-      destruct (eq_dec t0 t), (eq_dec t1 t0), (eq_dec t1 t); simpl; auto; try reflexivity;
-      rewrite -> e in e0; contradiction.
-    -  destruct t1, t2; try reflexivity; compute; destruct (eq_dec t0 t), (eq_dec t t0);
-       try reflexivity; auto; try contradiction; symmetry in e; contradiction.
+      simpl in *; auto; try reflexivity; compute; try destruct (eq_dec _ _); 
+      try reflexivity;
+      destruct (eq_dec t0 t), (eq_dec t1 t0), (eq_dec t1 t); simpl; auto; 
+      try reflexivity;
+      try (rewrite <- e in c; contradiction); now exfalso; eauto.
+    - destruct t1, t2; try reflexivity; compute; destruct (eq_dec t0 t), (eq_dec t t0);
+      try reflexivity; auto; try contradiction; symmetry in e; contradiction.
     - destruct t; reflexivity.
     - destruct x, y; simpl; firstorder; now inversion H.
     - now constructor.
@@ -338,11 +340,11 @@ Section Agreement.
   Proof.
     split; repeat intro.
     - ra_agree_destr; try firstorder; [|].
-      + rewrite -H1 H7 H2. reflexivity.
-      + rewrite H1 H7 -H2. reflexivity.
+      + find_rewrite3 t1 t2 t0 t. reflexivity.
+      + find_rewrite3 t2 t1 t t0. reflexivity.
     - ra_agree_destr; try firstorder; [|].
-      + rewrite H1 H3. reflexivity.
-      + rewrite -H3 H2. reflexivity.
+      + find_rewrite2 t1 t0 t. reflexivity.
+      + find_rewrite2 t0 t1 t. reflexivity.
     - ra_agree_destr; firstorder.
     - ra_agree_destr; firstorder.
     - ra_agree_destr; firstorder.
@@ -367,8 +369,8 @@ Section Agreement.
   Next Obligation.
     repeat intro. destruct n as [|n]; first by auto.
     ra_agree_destr; try firstorder.
-    - rewrite -H1 -H2. assumption.
-    - rewrite H1 H2. assumption.
+    - find_rewrite1 t1 t2. find_rewrite1 t t0. assumption.
+    - find_rewrite1 t2 t1. find_rewrite1 t0 t. assumption.
   Qed.
   Next Obligation.
     repeat intro. split.
@@ -378,7 +380,7 @@ Section Agreement.
       + intro. eapply dist_refl. intro. specialize (Hall n). destruct n as [|n]; first by apply: dist_bound.
         firstorder.
     - repeat intro. destruct n as [|n]; first by auto. ra_agree_destr; try firstorder.
-      + rewrite H0. reflexivity.
+      + find_rewrite1 t0 t. reflexivity.
   Qed.
   Next Obligation.
     repeat intro. destruct n as [|n]; first by auto.
@@ -387,7 +389,7 @@ Section Agreement.
   Next Obligation.
     repeat intro. destruct n as [|n]; first by auto.
     ra_agree_destr; try firstorder; [].
-    rewrite H1 -H2. reflexivity.
+    etransitivity; eassumption.
   Qed.
   Next Obligation.
     repeat intro. destruct n as [|n]; first by auto.

lib/ModuRes/UPred.v

-Require Import ssreflect.
+Require Import Ssreflect.ssreflect.
 Require Export PreoMet.
 
 Section Definitions.