diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /theories/Classes | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'theories/Classes')
-rw-r--r-- | theories/Classes/CMorphisms.v | 4 | ||||
-rw-r--r-- | theories/Classes/Equivalence.v | 8 | ||||
-rw-r--r-- | theories/Classes/Morphisms.v | 6 | ||||
-rw-r--r-- | theories/Classes/RelationPairs.v | 5 | ||||
-rw-r--r-- | theories/Classes/SetoidTactics.v | 16 |
5 files changed, 22 insertions, 17 deletions
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index c41eb2fa..1cfca416 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -452,7 +452,7 @@ Ltac partial_application_tactic := let rec do_partial_apps H m cont := match m with | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; - [(do_partial_apps H m' ltac:idtac)|clear H] + [(do_partial_apps H m' ltac:(idtac))|clear H] | _ => cont end in @@ -527,7 +527,7 @@ Hint Extern 7 (@Proper _ _ _) => proper_reflexive Section Normalize. Context (A : Type). - Class Normalizes (m : crelation A) (m' : crelation A) : Prop := + Class Normalizes (m : crelation A) (m' : crelation A) := normalizes : relation_equivalence m m'. (** Current strategy: add [flip] everywhere and reduce using [subrelation] diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index c4588947..80b0b7e4 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -49,11 +49,11 @@ Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope. (** Shortcuts to make proof search easier. *) -Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv. +Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv | 1. -Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv. +Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv | 1. -Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv. +Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv | 1. Next Obligation. Proof. intros A R sa x y z Hxy Hyz. @@ -123,7 +123,7 @@ Section Respecting. End Respecting. -(** The default equivalence on function spaces, with higher-priority than [eq]. *) +(** The default equivalence on function spaces, with higher priority than [eq]. *) Instance pointwise_reflexive {A} `(reflb : Reflexive B eqB) : Reflexive (pointwise_relation A eqB) | 9. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 8d942d90..06511ace 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -465,12 +465,12 @@ Ltac partial_application_tactic := let rec do_partial_apps H m cont := match m with | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; - [(do_partial_apps H m' ltac:idtac)|clear H] + [(do_partial_apps H m' ltac:(idtac))|clear H] | _ => cont end in let rec do_partial H ar m := - match ar with + lazymatch ar with | 0%nat => do_partial_apps H m ltac:(fail 1) | S ?n' => match m with @@ -483,7 +483,7 @@ Ltac partial_application_tactic := let n := fresh in evar (n:nat) ; let v := eval compute in n in clear n ; let H := fresh in - assert(H:Params m' v) by typeclasses eauto ; + assert(H:Params m' v) by (subst m'; once typeclasses eauto) ; let v' := eval compute in v in subst m'; (sk H v' || fail 1)) || fk diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index cbde5f9a..8d1c4982 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -43,6 +43,9 @@ Generalizable Variables A B RA RB Ri Ro f. Definition RelCompFun {A} {B : Type}(R:relation B)(f:A->B) : relation A := fun a a' => R (f a) (f a'). +(** Instances on RelCompFun must match syntactically *) +Typeclasses Opaque RelCompFun. + Infix "@@" := RelCompFun (at level 30, right associativity) : signature_scope. Notation "R @@1" := (R @@ Fst)%signature (at level 30) : signature_scope. @@ -65,6 +68,8 @@ Instance snd_measure : @Measure (A * B) B Snd. Definition RelProd {A : Type} {B : Type} (RA:relation A)(RB:relation B) : relation (A*B) := relation_conjunction (@RelCompFun (A * B) A RA fst) (RB @@2). +Typeclasses Opaque RelProd. + Infix "*" := RelProd : signature_scope. Section RelCompFun_Instances. diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 145d451f..190397ae 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -77,23 +77,23 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) Tactic Notation "setoid_replace" constr(x) "with" constr(y) "by" tactic3(t) := - setoidreplace (default_relation x y) ltac:t. + setoidreplace (default_relation x y) ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceat (default_relation x y) ltac:t o. + setoidreplaceat (default_relation x y) ltac:(t) o. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "by" tactic3(t) := - setoidreplacein (default_relation x y) id ltac:t. + setoidreplacein (default_relation x y) id ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceinat (default_relation x y) id ltac:t o. + setoidreplaceinat (default_relation x y) id ltac:(t) o. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) := @@ -107,13 +107,13 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "by" tactic3(t) := - setoidreplace (rel x y) ltac:t. + setoidreplace (rel x y) ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceat (rel x y) ltac:t o. + setoidreplaceat (rel x y) ltac:(t) o. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) @@ -130,14 +130,14 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "in" hyp(id) "by" tactic3(t) := - setoidreplacein (rel x y) id ltac:t. + setoidreplacein (rel x y) id ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "in" hyp(id) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceinat (rel x y) id ltac:t o. + setoidreplaceinat (rel x y) id ltac:(t) o. (** The [add_morphism_tactic] tactic is run at each [Add Morphism] command before giving the hand back to the user to discharge the |