aboutsummaryrefslogtreecommitdiff
path: root/contrib/correctness/psyntax.ml4
diff options
context:
space:
mode:
authorcorbinea2007-07-16 09:18:44 +0000
committercorbinea2007-07-16 09:18:44 +0000
commit4f7e1eb0f0c53ad9d5f93712af702a3b3c107f8d (patch)
treeaabfd317542ffb9f05e18f1b0d4d6f2b4d994ff8 /contrib/correctness/psyntax.ml4
parent935df5be8d2b487e17ab1609083b264477c19a4d (diff)
Generalized CAMLP4USE for pp dependencies
Removed parsing/lexer.ml4 special case No file depends on pa_extend_m.cmo anymore, Wierd ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10007 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/correctness/psyntax.ml4')
-rw-r--r--contrib/correctness/psyntax.ml41
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index f6aad378d8..72b609b24d 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -11,6 +11,7 @@
(* $Id$ *)
(*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4use: "pa_extend.cmo" i*)
open Options
open Util