From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id pBBDbLX1016096 for ; Sun, 11 Dec 2011 14:37:21 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AvcAAHyw5E5KfVI0imdsb2JhbABDhQelYQgiAQEBCgkNBxIGIYFyAQEBAwESAg8dATgBAwELAQUFBAEGNwICIhIBBQEcBicOh2aYLwqLHIMzg3KJLgIFDIpLgRYElHGNcT2BTYIt X-IronPort-AV: E=Sophos;i="4.71,335,1320620400"; d="scan'208";a="134907231" Received: from mail-ww0-f52.google.com ([74.125.82.52]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-MD5; 11 Dec 2011 14:37:16 +0100 Received: by wgbdr12 with SMTP id dr12so11188504wgb.9 for ; Sun, 11 Dec 2011 05:37:16 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; bh=CbOaSB+kIiV6xiyvJeJVknyeMpB0BOQoiuEoaBqKKO4=; b=jHTAAnACd2XcCJhI6wlqbfldB/2Hv4gSXkD7wEnN5/WC/QNoXVxYFNEMxAGw+fBlY6 nO/xcTGDtXUyPxaSjx5upE1Iq5KFnGM2ts2d/j4//rDI0fF7u+I2Qx+mf2fd87omDhN+ QdVhVPkMqdumu/NEfYO7gLQjsKmo8ZsP8oHpI= Received: by 10.180.14.69 with SMTP id n5mr18510495wic.13.1323610636299; Sun, 11 Dec 2011 05:37:16 -0800 (PST) MIME-Version: 1.0 Sender: arnaud.spiwack@gmail.com Received: by 10.227.173.65 with HTTP; Sun, 11 Dec 2011 05:36:35 -0800 (PST) In-Reply-To: <4EE4AFB8.5040509@frisch.fr> References: <55531934-37A5-4CC5-AB67-20CE4CCE8269@googlemail.com> <4EE37070.4010702@inria.fr> <1323541702.32136.8.camel@aurora> <1323550544.32136.19.camel@aurora> <4EE4AFB8.5040509@frisch.fr> From: Arnaud Spiwack Date: Sun, 11 Dec 2011 14:36:35 +0100 X-Google-Sender-Auth: vrjecXyckmXEeUPYOWWFEALsJdQ Message-ID: To: Alain Frisch Cc: Gabriel Scherer , Wojciech Meyer , =?UTF-8?B?SsOpcsOpbWllIERpbWlubw==?= , caml-list@inria.fr Content-Type: multipart/alternative; boundary=f46d040fa1c6cc2d1104b3d11d83 X-Validation-by: aspiwack@lix.polytechnique.fr Subject: Re: [Caml-list] Camlp4/p5 type reflection [was: OCaml maintenance status / community fork (again)] --f46d040fa1c6cc2d1104b3d11d83 Content-Type: text/plain; charset=UTF-8 > My understanding (please correct me if I'm wrong) is that Coq uses > camlp{4,5} only as an extensible parser library in order to parse its own > language (which can be extended with user-defined notations). In > particular, Coq does not use the following camlp{4,5} features: > This is not entirely correct. Coq uses camlp4's extensible ocaml syntax in quite a bit of its code. (though less than it use to, I hear). The following features are used: - the alternative representation of OCaml AST > - the Camlp4 grammar definitions for OCaml syntax(es) > - quotations/antiquotations to produce fragments of the OCaml AST > - OCaml syntax extensions to define grammar entries > - custom OCaml syntax extension for the Coq source code itself > Though quotations are used *very* sparsely (mostly in legacy code, they are not maintained). Arnaud Spiwack --f46d040fa1c6cc2d1104b3d11d83 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
My understand= ing (please correct me if I'm wrong) is that Coq uses camlp{4,5} only a= s an extensible parser library in order to parse its own language (which ca= n be extended with user-defined notations). In particular, Coq does not use= the following camlp{4,5} features:

This is not entirely correct. Coq uses camlp4's e= xtensible ocaml syntax in quite a bit of its code. (though less than it use= to, I hear). The following features are used:

=C2=A0- the alternative representation of OCaml AST
=C2=A0- the Camlp4 grammar definitions for OCaml syntax(es)
=C2=A0- quotations/antiquotations to produce fragments of the OCaml AST
=C2=A0- OCaml syntax extensions to define grammar entries
=C2=A0- custom OCaml syntax extension for the Coq source code itself

Though quotations are used *very* sparsely (mostly in l= egacy code, they are not maintained).







Arnaud= Spiwack

--f46d040fa1c6cc2d1104b3d11d83--