diff options
| author | corbinea | 2003-03-31 11:57:52 +0000 |
|---|---|---|
| committer | corbinea | 2003-03-31 11:57:52 +0000 |
| commit | d8da8cb7b9af7df65f63af30bfa5775531426165 (patch) | |
| tree | 869c7417522fda3f075402aa44199edc20f17ad2 /tactics/setoid_replace.ml | |
| parent | 516a349d32dde37d8382df89733662a4e1ad9576 (diff) | |
factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3815 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/setoid_replace.ml')
| -rw-r--r-- | tactics/setoid_replace.ml | 20 |
1 files changed, 3 insertions, 17 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 4468fd4d35..e397cd0cfe 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -47,23 +47,9 @@ type morphism = let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c -let constant dir s = - let dir = make_dirpath - (List.map id_of_string (List.rev ("Coq"::"Setoids"::dir))) in - let id = id_of_string s in - try - Declare.global_reference_in_absolute_module dir id - with Not_found -> - anomaly ("Setoid: cannot find "^(string_of_qualid (make_qualid dir id))) - -let global_constant dir s = - let dir = make_dirpath - (List.map id_of_string (List.rev ("Coq"::"Init"::dir))) in - let id = id_of_string s in - try - Declare.global_reference_in_absolute_module dir id - with Not_found -> - anomaly ("Setoid: cannot find "^(string_of_qualid (make_qualid dir id))) +let constant dir s = Coqlib.gen_constant "Setoid_replace" ("Setoids"::dir) s + +let global_constant dir s =Coqlib.gen_constant "Setoid_replace" ("Init"::dir) s let current_constant id = try |