diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-15 15:53:27 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-15 15:53:27 +0000 |
| commit | a81f52f601c9851d59d0a9f53f0a46c7444fcab1 (patch) | |
| tree | ff49d0f23739789e57801b2c6f5e63ee9b38c85a /tactics/class_tactics.ml4 | |
| parent | ecdaf627e4ab97611a0cbabab8b30b7055110682 (diff) | |
Document CHANGES in setoid rewrite, move DefaultRelation to
SetoidTactics and document it. Cleanup Classes.Equivalence.
Minor fixes to the Program doc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10799 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/class_tactics.ml4')
| -rw-r--r-- | tactics/class_tactics.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index a54de8b8a..96b3aff76 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -502,7 +502,7 @@ let respectful_dep = lazy (gen_constant ["Classes"; "Morphisms"] "respectful_dep let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful") let equivalence = lazy (gen_constant ["Classes"; "RelationClasses"] "Equivalence") -let default_relation = lazy (gen_constant ["Classes"; "RelationClasses"] "DefaultRelation") +let default_relation = lazy (gen_constant ["Classes"; "SetoidTactics"] "DefaultRelation") let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation") let mk_relation a = mkApp (Lazy.force coq_relation, [| a |]) @@ -1144,7 +1144,7 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = init_setoid (); match (refl,symm,trans) with (None, None, None) -> - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.DefaultRelation" + let instance = declare_instance a aeq n "Coq.Classes.SetoidTactics.DefaultRelation" in ignore(anew_instance binders instance []) | (Some lemma1, None, None) -> ignore (declare_instance_refl binders a aeq n lemma1) |