From 25533df336888df4255e3882e21d5d5420e5de28 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 9 Jul 2010 17:40:36 +0000 Subject: Finish adding out-of-the-box support for camlp4 If you want to try, it should be now as simple as: make clean && ./configure -local -usecamlp4 && make For the moment, the default stays camlp5, hence ./configure -usecamlp5 and ./configure are equivalent. Thanks to a suggestion by N. Pouillard, the remaining incompatibilities are now handled via some token filtering in camlp4. See compat5*.mlp. Morally, these files should be named .ml4, but I prefer having them not in $(...ML4) variables, it might confuse the Makefile... The empty compat5*.ml are used to build empty .cmo for making camlp5 happy. For camlp4, - tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded - tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with syntax such that VERNAC EXTEND, we only load it for a few files via camlp4deps TODO: check that my quick adaptation of camlp5-specific code in tactics/extratactics.ml4 is ok. It seems the code by Chung-Kil Hur is hiding information in the locations ?! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13274 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/argextend.ml4 | 2 ++ parsing/q_constr.ml4 | 2 ++ parsing/tacextend.ml4 | 2 ++ parsing/vernacextend.ml4 | 2 ++ 4 files changed, 8 insertions(+) (limited to 'parsing') diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index e156bdc26..fc1f05dad 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4deps: "tools/compat5b.cmo" i*) + open Genarg open Q_util open Egrammar diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index fb34a5aa2..43f455924 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4deps: "tools/compat5b.cmo" i*) + open Rawterm open Term open Names diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index f64c8f700..3aac36c08 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4deps: "tools/compat5b.cmo" i*) + open Util open Genarg open Q_util diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 1fa0e7e99..9ed89536c 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4deps: "tools/compat5b.cmo" i*) + open Util open Genarg open Q_util -- cgit v1.2.3