diff options
| -rw-r--r-- | tactics/class_tactics.ml4 | 30 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 30 |
2 files changed, 30 insertions, 30 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 96b3aff76..922539ddb 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -508,11 +508,11 @@ let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "rela let mk_relation a = mkApp (Lazy.force coq_relation, [| a |]) let coq_relationT = lazy (gen_constant ["Classes";"Relations"] "relationT") -let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "equivalence_reflexive") +let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "Equivalence_Reflexive") let setoid_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv") let setoid_morphism = lazy (gen_constant ["Classes"; "SetoidClass"] "setoid_morphism") -let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "equivalence_reflexive") +let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "Equivalence_Reflexive") let arrow_morphism a b = if isprop a && isprop b then @@ -1124,17 +1124,17 @@ let init_setoid () = check_required_library ["Coq";"Setoids";"Setoid"] let declare_instance_refl binders a aeq n lemma = - let instance = declare_instance a aeq (add_suffix n "_reflexive") "Coq.Classes.RelationClasses.Reflexive" + let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" in anew_instance binders instance [((dummy_loc,id_of_string "reflexivity"),[],lemma)] let declare_instance_sym binders a aeq n lemma = - let instance = declare_instance a aeq (add_suffix n "_symmetric") "Coq.Classes.RelationClasses.Symmetric" + let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric" in anew_instance binders instance [((dummy_loc,id_of_string "symmetry"),[],lemma)] let declare_instance_trans binders a aeq n lemma = - let instance = declare_instance a aeq (add_suffix n "_transitive") "Coq.Classes.RelationClasses.Transitive" + let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive" in anew_instance binders instance [((dummy_loc,id_of_string "transitivity"),[],lemma)] @@ -1161,16 +1161,16 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in ignore( anew_instance binders instance - [((dummy_loc,id_of_string "preorder_reflexive"), [], mkIdentC lemma_refl); - ((dummy_loc,id_of_string "preorder_transitive"),[], mkIdentC lemma_trans)]) + [((dummy_loc,id_of_string "PreOrder_Reflexive"), [], mkIdentC lemma_refl); + ((dummy_loc,id_of_string "PreOrder_Transitive"),[], mkIdentC lemma_trans)]) | (None, Some lemma2, Some lemma3) -> let lemma_sym = declare_instance_sym binders a aeq n lemma2 in let lemma_trans = declare_instance_trans binders a aeq n lemma3 in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in ignore( anew_instance binders instance - [((dummy_loc,id_of_string "per_symmetric"), [], mkIdentC lemma_sym); - ((dummy_loc,id_of_string "per_transitive"),[], mkIdentC lemma_trans)]) + [((dummy_loc,id_of_string "PER_Symmetric"), [], mkIdentC lemma_sym); + ((dummy_loc,id_of_string "PER_Transitive"),[], mkIdentC lemma_trans)]) | (Some lemma1, Some lemma2, Some lemma3) -> let lemma_refl = declare_instance_refl binders a aeq n lemma1 in let lemma_sym = declare_instance_sym binders a aeq n lemma2 in @@ -1178,9 +1178,9 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance binders instance - [((dummy_loc,id_of_string "equivalence_reflexive"), [], mkIdentC lemma_refl); - ((dummy_loc,id_of_string "equivalence_symmetric"), [], mkIdentC lemma_sym); - ((dummy_loc,id_of_string "equivalence_transitive"),[], mkIdentC lemma_trans)]) + [((dummy_loc,id_of_string "Equivalence_Reflexive"), [], mkIdentC lemma_refl); + ((dummy_loc,id_of_string "Equivalence_Symmetric"), [], mkIdentC lemma_sym); + ((dummy_loc,id_of_string "Equivalence_Transitive"),[], mkIdentC lemma_trans)]) type 'a binders_let_argtype = (local_binder list, 'a) Genarg.abstract_argument_type @@ -1355,9 +1355,9 @@ let add_setoid binders a aeq t n = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance binders instance - [((dummy_loc,id_of_string "equivalence_reflexive"), [], mkIdentC lemma_refl); - ((dummy_loc,id_of_string "equivalence_symmetric"), [], mkIdentC lemma_sym); - ((dummy_loc,id_of_string "equivalence_transitive"),[], mkIdentC lemma_trans)]) + [((dummy_loc,id_of_string "Equivalence_Reflexive"), [], mkIdentC lemma_refl); + ((dummy_loc,id_of_string "Equivalence_Symmetric"), [], mkIdentC lemma_sym); + ((dummy_loc,id_of_string "Equivalence_Transitive"),[], mkIdentC lemma_trans)]) let add_morphism_infer m n = init_setoid (); diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 6a002d97a..a57914fdd 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -133,34 +133,34 @@ Ltac obligations_tactic ::= simpl_relation. (** Logical implication. *) -Program Instance impl_reflexive : Reflexive impl. -Program Instance impl_transitive : Transitive impl. +Program Instance impl_Reflexive : Reflexive impl. +Program Instance impl_Transitive : Transitive impl. (** Logical equivalence. *) -Program Instance iff_reflexive : Reflexive iff. -Program Instance iff_symmetric : Symmetric iff. -Program Instance iff_transitive : Transitive iff. +Program Instance iff_Reflexive : Reflexive iff. +Program Instance iff_Symmetric : Symmetric iff. +Program Instance iff_Transitive : Transitive iff. (** Leibniz equality. *) -Program Instance eq_reflexive : Reflexive (@eq A). -Program Instance eq_symmetric : Symmetric (@eq A). -Program Instance eq_transitive : Transitive (@eq A). +Program Instance eq_Reflexive : Reflexive (@eq A). +Program Instance eq_Symmetric : Symmetric (@eq A). +Program Instance eq_Transitive : Transitive (@eq A). (** Various combinations of reflexivity, symmetry and transitivity. *) (** A [PreOrder] is both Reflexive and Transitive. *) Class PreOrder A (R : relation A) := - preorder_reflexive :> Reflexive R ; - preorder_transitive :> Transitive R. + PreOrder_Reflexive :> Reflexive R ; + PreOrder_Transitive :> Transitive R. (** A partial equivalence relation is Symmetric and Transitive. *) Class PER (carrier : Type) (pequiv : relation carrier) := - per_symmetric :> Symmetric pequiv ; - per_transitive :> Transitive pequiv. + PER_Symmetric :> Symmetric pequiv ; + PER_Transitive :> Transitive pequiv. (** We can build a PER on the Coq function space if we have PERs on the domain and codomain. *) @@ -179,9 +179,9 @@ Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] => (** The [Equivalence] typeclass. *) Class Equivalence (carrier : Type) (equiv : relation carrier) := - equivalence_reflexive :> Reflexive equiv ; - equivalence_symmetric :> Symmetric equiv ; - equivalence_transitive :> Transitive equiv. + Equivalence_Reflexive :> Reflexive equiv ; + Equivalence_Symmetric :> Symmetric equiv ; + Equivalence_Transitive :> Transitive equiv. (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *) |