diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrsetoid.v | 86 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 6 |
2 files changed, 4 insertions, 88 deletions
diff --git a/plugins/ssr/ssrsetoid.v b/plugins/ssr/ssrsetoid.v index 609c9d5ab8..7c5cd135fe 100644 --- a/plugins/ssr/ssrsetoid.v +++ b/plugins/ssr/ssrsetoid.v @@ -18,9 +18,7 @@ than [eq] or [iff], e.g. a [RewriteRelation], by doing: [Require Import ssreflect. Require Setoid.] - This file's instances have priority 12 > other stdlib instances - and each [Under_rel] instance comes with a [Hint Cut] directive - (otherwise Ring_polynom.v won't compile because of unbounded search). + This file's instances have priority 12 > other stdlib instances. (Note: this file could be skipped when porting [under] to stdlib2.) *) @@ -38,85 +36,3 @@ Instance compat_Reflexive : RelationClasses.Reflexive R -> ssrclasses.Reflexive R | 12. Proof. now trivial. Qed. - -(** Add instances so that ['Under[ F i ]] terms, - that is, [Under_rel T R (F i) (?G i)] terms, - can be manipulated with rewrite/setoid_rewrite with lemmas on [R]. - Note that this requires that [R] is a [Prop] relation, otherwise - a [bool] relation may need to be "lifted": see the [TestPreOrder] - section in test-suite/ssr/under.v *) - -Instance Under_subrelation {A} (R : relation A) : subrelation R (Under_rel _ R) | 12. -Proof. now rewrite Under_relE. Qed. - -(* see also Morphisms.trans_co_eq_inv_impl_morphism *) - -Instance Under_Reflexive {A} (R : relation A) : - RelationClasses.Reflexive R -> - RelationClasses.Reflexive (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Reflexive Under_Reflexive] : typeclass_instances. - -(* These instances are a bit off-topic given that (Under_rel A R) will - typically be reflexive, to be able to trigger the [over] terminator - -Instance under_Irreflexive {A} (R : relation A) : - RelationClasses.Irreflexive R -> - RelationClasses.Irreflexive (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Irreflexive Under_Irreflexive] : typeclass_instances. - -Instance under_Asymmetric {A} (R : relation A) : - RelationClasses.Asymmetric R -> - RelationClasses.Asymmetric (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Asymmetric Under_Asymmetric] : typeclass_instances. - -Instance under_StrictOrder {A} (R : relation A) : - RelationClasses.StrictOrder R -> - RelationClasses.StrictOrder (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Strictorder Under_Strictorder] : typeclass_instances. - *) - -Instance Under_Symmetric {A} (R : relation A) : - RelationClasses.Symmetric R -> - RelationClasses.Symmetric (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Symmetric Under_Symmetric] : typeclass_instances. - -Instance Under_Transitive {A} (R : relation A) : - RelationClasses.Transitive R -> - RelationClasses.Transitive (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Transitive Under_Transitive] : typeclass_instances. - -Instance Under_PreOrder {A} (R : relation A) : - RelationClasses.PreOrder R -> - RelationClasses.PreOrder (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_PreOrder Under_PreOrder] : typeclass_instances. - -Instance Under_PER {A} (R : relation A) : - RelationClasses.PER R -> - RelationClasses.PER (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_PER Under_PER] : typeclass_instances. - -Instance Under_Equivalence {A} (R : relation A) : - RelationClasses.Equivalence R -> - RelationClasses.Equivalence (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Equivalence Under_Equivalence] : typeclass_instances. - -(* Don't handle Antisymmetric and PartialOrder classes for now, - as these classes depend on two relation symbols... *) diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 9f6fe0e651..d8dbf2f3dc 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -370,14 +370,14 @@ let coerce_search_pattern_to_sort hpat = let filter_head, coe_path = try let _, cp = - Classops.lookup_path_to_sort_from (push_rels_assum dc env) sigma ht in + Coercionops.lookup_path_to_sort_from (push_rels_assum dc env) sigma ht in warn (); true, cp with _ -> false, [] in let coerce hp coe_index = - let coe_ref = coe_index.Classops.coe_value in + let coe_ref = coe_index.Coercionops.coe_value in try - let n_imps = Option.get (Classops.hide_coercion coe_ref) in + let n_imps = Option.get (Coercionops.hide_coercion coe_ref) in mkPApp (Pattern.PRef coe_ref) n_imps [|hp|] with Not_found | Option.IsNone -> errorstrm (str "need explicit coercion " ++ pr_global coe_ref ++ spc () |