diff options
| author | clrenard | 2001-09-18 13:09:47 +0000 |
|---|---|---|
| committer | clrenard | 2001-09-18 13:09:47 +0000 |
| commit | b915d23eefe20c6ca9d744807c9c18b91d9fc1df (patch) | |
| tree | 5586f10324661711386ebaccda28dccb0f1e9514 /tactics/setoid_replace.ml | |
| parent | 1f78733204d5a1232d06c103057dc65dcb14a7ea (diff) | |
Modification de l'emplacement des fichiers pour les setoides.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1982 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/setoid_replace.ml')
| -rw-r--r-- | tactics/setoid_replace.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 613c0a475c..f7eb0bbd42 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -39,7 +39,7 @@ type morphism = let constr_of c = Astterm.interp_constr Evd.empty (Global.env()) c let constant dir s = - let dir = make_dirpath (List.map id_of_string ("Coq"::"Setoid"::dir)) in + let dir = make_dirpath (List.map id_of_string ("Coq"::"Init"::dir)) in let id = id_of_string s in try Declare.global_reference_in_absolute_module dir id @@ -62,13 +62,13 @@ let current_constant id = (* Setoid_theory *) -let coq_Setoid_Theory = lazy(constant ["Setoid_replace"] "Setoid_Theory") +let coq_Setoid_Theory = lazy(constant ["Setoid"] "Setoid_Theory") -let coq_seq_refl = lazy(constant ["Setoid_replace"] "Seq_refl") -let coq_seq_sym = lazy(constant ["Setoid_replace"] "Seq_sym") -let coq_seq_trans = lazy(constant ["Setoid_replace"] "Seq_trans") +let coq_seq_refl = lazy(constant ["Setoid"] "Seq_refl") +let coq_seq_sym = lazy(constant ["Setoid"] "Seq_sym") +let coq_seq_trans = lazy(constant ["Setoid"] "Seq_trans") -let coq_fleche = lazy(constant ["Setoid_replace"] "fleche") +let coq_fleche = lazy(constant ["Setoid"] "fleche") (* Coq constants *) |