diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-22 21:32:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-22 21:32:03 +0000 |
| commit | 937ca7a6dbc1a031b7c4540c665b8774440c1bb9 (patch) | |
| tree | 3a2c73669cb40011c2e62a11d3364d39f74040ba /contrib/omega | |
| parent | de9150e6033467fd2fa8fc93d5f057e8c2f6537f (diff) | |
Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 'section_path' pour les noms absolus
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/omega')
| -rw-r--r-- | contrib/omega/coq_omega.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index bdf4544f9..3b2dff70d 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -207,9 +207,7 @@ let recognize_number t = To use the constant Zplus, one must type "Lazy.force coq_Zplus" This is the right way to access to Coq constants in tactics ML code *) -let constant dir id = - Declare.global_qualified_reference - (make_path dir (id_of_string id) CCI) +let constant dir s = Declare.global_qualified_reference (make_qualid dir s) (* fast_integer *) let coq_xH = lazy (constant ["fast_integer"] "xH") |