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 /contrib/ring | |
| 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/ring')
| -rw-r--r-- | contrib/ring/quote.ml | 10 | ||||
| -rw-r--r-- | contrib/ring/ring.ml | 9 |
2 files changed, 2 insertions, 17 deletions
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index a2798d7a75..393eff193f 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -119,15 +119,7 @@ open Tacexpr We do that lazily, because this code can be linked before the constants are loaded in the environment *) -let constant dir s = - let dir = make_dirpath - (List.map id_of_string (List.rev ("Coq"::"ring"::dir))) in - let id = id_of_string s in - try - Declare.global_reference_in_absolute_module dir id - with Not_found -> - anomaly ("Quote: cannot find "^ - (Libnames.string_of_qualid (Libnames.make_qualid dir id))) +let constant dir s = Coqlib.gen_constant "Quote" ("ring"::dir) s let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm") let coq_Node_vm = lazy (constant ["Quote"] "Node_vm") diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index f4848c729e..c360f795a2 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -38,14 +38,7 @@ open Quote let mt_evd = Evd.empty let constr_of c = Constrintern.interp_constr mt_evd (Global.env()) c -let constant dir s = - let dir = make_dirpath (List.map id_of_string (List.rev ("Coq"::dir))) in - let id = id_of_string s in - try - Declare.global_reference_in_absolute_module dir id - with Not_found -> - anomaly ("Ring: cannot find "^ - (Libnames.string_of_qualid (Libnames.make_qualid dir id))) +let constant = Coqlib.gen_constant "Ring" (* Ring theory *) let coq_Ring_Theory = lazy (constant ["ring";"Ring_theory"] "Ring_Theory") |