From 95f8a0ac38cbd792a0b5d8006aac1ef1a9f70da8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 17 Apr 2003 15:00:24 +0000
Subject: commentaires

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3938 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/omega/coq_omega.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 6f988076ef..501206c88d 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -304,15 +304,13 @@ let coq_Zne = lazy (zarith_constant ["auxiliary"] "Zne")
 (* Peano *)
 let coq_le = lazy (constant ["Init";"Peano"] "le")
 let coq_gt = lazy (constant ["Init";"Peano"] "gt")
+let coq_minus = lazy (constant ["Init";"Peano"] "minus")
 
 (* Datatypes *)
 let coq_nat = lazy (constant ["Init";"Datatypes"] "nat")
 let coq_S = lazy (constant ["Init";"Datatypes"] "S")
 let coq_O = lazy (constant ["Init";"Datatypes"] "O")
 
-(* Minus *)
-let coq_minus = lazy (constant ["Init";"Peano"] "minus")
-
 (* Compare_dec *)
 let coq_le_gt_dec = lazy (constant ["Arith";"Compare_dec"] "le_gt_dec")
 let coq_dec_eq_nat = lazy (constant ["Arith";"Peano_dec"] "dec_eq_nat")
-- 
cgit v1.2.3