diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-31 11:57:52 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-31 11:57:52 +0000 |
| commit | d8da8cb7b9af7df65f63af30bfa5775531426165 (patch) | |
| tree | 869c7417522fda3f075402aa44199edc20f17ad2 /contrib/field/field.ml4 | |
| 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 'contrib/field/field.ml4')
| -rw-r--r-- | contrib/field/field.ml4 | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index c67dea9aa..6f5668b19 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -26,15 +26,7 @@ open Tacexpr let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c (* Construction of constants *) -let constant dir s = - let dir = make_dirpath - (List.map id_of_string (List.rev ("Coq"::"field"::dir))) in - let id = id_of_string s in - try - Declare.global_reference_in_absolute_module dir id - with Not_found -> - anomaly ("Field: cannot find "^ - (Libnames.string_of_qualid (Libnames.make_qualid dir id))) +let constant dir s = Coqlib.gen_constant "Field" ("field"::dir) s (* To deal with the optional arguments *) let constr_of_opt a opt = |