aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/omega
diff options
context:
space:
mode:
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")