# HG changeset patch
# User wenzelm
# Date 1297195563 -3600
# Node ID 775da08dae1b695b460d468899f109b04f79d9ff
# Parent  996b0c14a430bbe3b08f877cea2b9f039fb0205f
clarified comment -- ancienct PG 3.7.x is still in use;

diff -r 996b0c14a430 -r 775da08dae1b src/Pure/ProofGeneral/pgip_types.ML
--- a/src/Pure/ProofGeneral/pgip_types.ML	Tue Feb 08 20:59:12 2011 +0100
+++ b/src/Pure/ProofGeneral/pgip_types.ML	Tue Feb 08 21:06:03 2011 +0100
@@ -273,7 +273,7 @@
                     | Pgipbool => "pgipbool"
                     | Pgipint _ => "pgipint"
                     | Pgipnat => "pgipint"
-                    | Pgipreal => "pgipint"  (* FIXME sic? *)
+                    | Pgipreal => "pgipint"  (*sic!*)  (*required for PG 4.0 and 3.7.x*)
                     | Pgipstring => "pgipstring"
                     | Pgipconst _ => "pgipconst"
                     | Pgipchoice _ => "pgipchoice"