upgrade mathcomp

_CoqProject

@@ -4,25 +4,25 @@
 
 core/options.v
 core/axioms.v
-core/auto.v
 core/prelude.v
 core/pred.v
-core/ordtype.v
-core/seqperm.v
-core/finmap.v
-core/rtc.v
+core/auto.v
 core/seqext.v
 core/slice.v
-core/useqord.v
 core/uslice.v
+core/useqord.v
 core/uconsec.v
+core/ordtype.v
+core/seqperm.v
+core/finmap.v
+core/rtc.v
 pcm/pcm.v
 pcm/autopcm.v
 pcm/morphism.v
 pcm/invertible.v
 pcm/unionmap.v
+pcm/natmap.v
 pcm/automap.v
 pcm/heap.v
 pcm/mutex.v
-pcm/lift.v
-pcm/natmap.v
+

core/auto.v

@@ -1,3 +1,16 @@
+(*
+Copyright 2013 IMDEA Software Institute
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+    http://www.apache.org/licenses/LICENSE-2.0
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+*)
+
 From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat seq eqtype.
 From pcm Require Import options prelude.
@@ -50,6 +63,7 @@ Variable A : Type.
 
 Structure tagged_elem := XTag {xuntag :> A}.
 
+
 Definition extend_tag := XTag.
 Definition recurse_tag := extend_tag.
 Canonical found_tag x := recurse_tag x.
@@ -61,7 +75,7 @@ Canonical found_tag x := recurse_tag x.
 (* - i : output index of pivot in xs2                               *)
 
 Definition axiom xs1 xs2 i (pivot : tagged_elem) :=
-  onth xs2 i = Some (xuntag pivot) /\ prefix xs1 xs2.
+  onth xs2 i = Some (xuntag pivot) /\ Prefix xs1 xs2.
 Structure xfind (xs1 xs2 : seq A) (i : nat) :=
   Form {pivot :> tagged_elem; _ : axiom xs1 xs2 i pivot}.
 
@@ -73,12 +87,12 @@ Canonical found_form x t := Form (@found_pf x t).
 (* recurse *)
 Lemma recurse_pf i x xs1 xs2 (f : xfind xs1 xs2 i) :
         axiom (x :: xs1) (x :: xs2) i.+1 (recurse_tag (xuntag f)).
-Proof. by case: f=>pv [H1 H2]; split=>//; apply/prefix_cons. Qed.
+Proof. by case: f=>pv [H1 H2]; split=>//; apply/Prefix_cons. Qed.
 Canonical recurse_form i x xs1 xs2 f := Form (@recurse_pf i x xs1 xs2 f).
 
 (* failed to find; attach the element to output *)
 Lemma extend_pf x : axiom [::] [:: x] 0 (extend_tag x).
 Proof. by []. Qed.
 Canonical extend_form x := Form (@extend_pf x).
 
-End XFind.
+End XFind.

core/axioms.v

@@ -22,6 +22,7 @@ limitations under the License.
 (******************************************************************************)
 
 From Coq Require Import ssreflect ssrfun Eqdep ClassicalFacts.
+From mathcomp Require Import eqtype.
 From pcm Require Import options.
 
 (*****************************)
@@ -37,7 +38,7 @@ Axiom fext : forall A (B : A -> Type) (f1 f2 : forall x, B x),
                (forall x, f1 x = f2 x) -> f1 = f2.
 
 Lemma pf_irr (P : Prop) (p1 p2 : P) : p1 = p2.
-Proof. by apply/ext_prop_dep_proof_irrel_cic/pext. Qed.
+Proof. by apply/ext_prop_dep_proof_irrel_cic/@pext. Qed.
 
 Lemma sval_inj A P : injective (@sval A P).
 Proof.
@@ -93,13 +94,20 @@ End Cast.
 Arguments cast {T} interp [A][B] pf v.
 Arguments jmeq {T} interp [A][B] v w.
 
-#[export]
-Hint Resolve jm_refl : core.
+#[export] Hint Resolve jm_refl : core.
 
 (* special notation for the common case when interp = id *)
 Notation icast pf v := (@cast _ id _ _ pf v).
 Notation ijmeq v w := (@jmeq _ id _ _ v w).
 
+(* in case of eqTypes StreicherK not needed *)
+Section EqTypeCast.
+Variable (T : eqType) (interp : T -> Type).
+Lemma eqd a (pf : a = a) (v : interp a) : cast interp pf v = v.
+Proof. by rewrite eq_axiomK. Qed.
+End EqTypeCast.
+
+
 (* type dynamic is sigT *)
 
 Section Dynamic.