aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/omega
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-29 14:16:59 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-29 14:16:59 +0000
commitff663b22854f1f609de7e0cc34dd67a73f4fcb9b (patch)
tree23b4d89e7be26760419a2e74ecaff202abab7d7e /contrib/omega
parentdb2919d5c2d664ba0f09781aa7332dd2d8ffa725 (diff)
Changement dans les noms longs (2eme)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1028 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/omega')
-rw-r--r--contrib/omega/coq_omega.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 20dd7dd05..c874e135a 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -213,7 +213,7 @@ let recognize_number t =
let constant dir s =
Declare.global_absolute_reference
- (make_path ("Zarith"::dir) (id_of_string s) CCI)
+ (make_path ("Coq"::"Zarith"::dir) (id_of_string s) CCI)
(* fast_integer *)
let coq_xH = lazy (constant ["fast_integer"] "xH")