diff options
| author | msozeau | 2008-03-16 13:40:45 +0000 |
|---|---|---|
| committer | msozeau | 2008-03-16 13:40:45 +0000 |
| commit | a76ad2ccdc57f54bd23e1c64f3f4a4af8e912050 (patch) | |
| tree | 07f989e72b672b508e09f820ab3c32a4016698fe /tactics | |
| parent | b149e6e21f68d0851f4387dd7182aaca2021041d (diff) | |
Reorganize Program and Classes theories. Requiring Setoid no longer sets
implicits for left, inl or eq, hence some theories had to be changed
again. It should make some user contribs compile again too. Also
do not import functional extensionality when importing Program.Basics,
add a Combinators file for proofs requiring it and a Syntax file for the
implicit settings. Move Classes.Relations to Classes.RelationClasses to
avoid name clash warnings as advised by Hugo and Pierre.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10681 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 25 |
1 files changed, 11 insertions, 14 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 8f11989a1b..71ab3a5f7c 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -360,28 +360,25 @@ let impl = lazy (gen_constant ["Program"; "Basics"] "impl") let arrow = lazy (gen_constant ["Program"; "Basics"] "arrow") let coq_id = lazy (gen_constant ["Program"; "Basics"] "id") -let reflexive_type = lazy (gen_constant ["Classes"; "Relations"] "Reflexive") -let reflexive_proof = lazy (gen_constant ["Classes"; "Relations"] "reflexive") +let reflexive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "Reflexive") +let reflexive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "reflexive") -let symmetric_type = lazy (gen_constant ["Classes"; "Relations"] "Symmetric") -let symmetric_proof = lazy (gen_constant ["Classes"; "Relations"] "symmetric") +let symmetric_type = lazy (gen_constant ["Classes"; "RelationClasses"] "Symmetric") +let symmetric_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "symmetric") -let transitive_type = lazy (gen_constant ["Classes"; "Relations"] "Transitive") -let transitive_proof = lazy (gen_constant ["Classes"; "Relations"] "transitive") +let transitive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "Transitive") +let transitive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "transitive") -let inverse = lazy (gen_constant ["Classes"; "Relations"] "inverse") +let inverse = lazy (gen_constant ["Classes"; "RelationClasses"] "inverse") let respectful_dep = lazy (gen_constant ["Classes"; "Morphisms"] "respectful_dep") let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful") -let equivalence = lazy (gen_constant ["Classes"; "Relations"] "Equivalence") -let default_relation = lazy (gen_constant ["Classes"; "Relations"] "DefaultRelation") +let equivalence = lazy (gen_constant ["Classes"; "RelationClasses"] "Equivalence") +let default_relation = lazy (gen_constant ["Classes"; "RelationClasses"] "DefaultRelation") -let iff_equiv = lazy (gen_constant ["Classes"; "Relations"] "iff_equivalence") -let eq_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "eq_equivalence") - -(* let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation") *) -let coq_relation = lazy (gen_constant ["Classes";"Relations"] "relation") +(* let coq_relation = lazy (gen_constant ["RelationClasses";"Relation_Definitions"] "relation") *) +let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation") let coq_relation a = mkApp (Lazy.force coq_relation, [| a |]) let coq_relationT = lazy (gen_constant ["Classes";"Relations"] "relationT") |