diff options
| author | herbelin | 2000-11-29 14:08:36 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-29 14:08:36 +0000 |
| commit | db2919d5c2d664ba0f09781aa7332dd2d8ffa725 (patch) | |
| tree | 9fab92fb15eed039f7a2985d1eab481ef23670e9 | |
| parent | 0f1706ba8646812f612f67a5002a735fd5d1af74 (diff) | |
Changement dans les noms longs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1027 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/omega/coq_omega.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 51d9a46ecb..20dd7dd05c 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -339,7 +339,8 @@ let coq_neq = lazy (constant ["auxiliary"] "neq") let coq_Zne = lazy (constant ["auxiliary"] "Zne") let constant dir s = - Declare.global_absolute_reference (make_path dir (id_of_string s) CCI) + Declare.global_absolute_reference + (make_path ("Coq"::dir) (id_of_string s) CCI) (* Peano *) let coq_le = lazy (constant ["Init";"Peano"] "le") |