From a6e84aec738f129e35fed9ae9a8d556f04a62d6c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 15 Dec 2002 12:05:16 +0000
Subject: Pas de 0 dans positive

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3438 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_zsyntax.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index 62a2f422a3..5103aedb0f 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -171,10 +171,10 @@ let pos_of_bignat dloc x =
   pos_of x
 
 let interp_positive dloc = function
-  | POS n -> pos_of_bignat dloc n
-  | NEG n ->
+  | POS n when is_nonzero n -> pos_of_bignat dloc n
+  | _ ->
       user_err_loc (dloc, "interp_positive",
-        str "No negative number in type \"positive\"!")
+        str "Only strictly positive numbers in type \"positive\"!")
 
 let rec pat_pos_of_bignat dloc x name =
   match div2_with_rest x with
-- 
cgit v1.2.3