Integration of Jacques-Henri Jourdan's verified parser.

(Merge of branch newparser.)


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 0 insertions, 5 deletions

diff --git a/cparser/GCC.ml b/cparser/GCC.ml
index 17b718b..1bcbbbc 100644
--- a/cparser/GCC.ml
+++ b/cparser/GCC.ml
@@ -201,11 +201,6 @@ let builtins = {
   "__builtin_strncpy",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
   "__builtin_strspn",  (intType, [ charConstPtrType; charConstPtrType ], false);
   "__builtin_strpbrk",  (charPtrType, [ charConstPtrType; charConstPtrType ], false);
-  (* When we parse builtin_types_compatible_p, we change its interface *)
-  "__builtin_types_compatible_p", 
-                              (intType, [ uintType; (* Sizeof the type *)
-                                          uintType  (* Sizeof the type *) ],
-                               false);
   "__builtin_tan",  (doubleType, [ doubleType ], false);
   "__builtin_tanf",  (floatType, [ floatType ], false);
   "__builtin_tanl",  (longDoubleType, [ longDoubleType ], false);