diff options
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 |