diff --git a/math/coq/Makefile b/math/coq/Makefile
index 47a5666d455..ab42fc5f7a0 100644
--- a/math/coq/Makefile
+++ b/math/coq/Makefile
@@ -1,4 +1,4 @@
-# $OpenBSD: Makefile,v 1.5 2002/11/04 21:10:44 naddy Exp $
+# $OpenBSD: Makefile,v 1.6 2002/12/18 09:40:07 sturm Exp $
 
 COMMENT=		"proof assistant based on a typed lambda calculus"
 
@@ -31,19 +31,16 @@ EXTRACT_ONLY=		${DISTNAME}.tar.gz \
 			doc-html.tar.gz \
 			library.tar.gz  \
 
-BUILD_DEPENDS=		::lang/ocaml
-
 FAKE_FLAGS=		COQINSTALLPREFIX=${WRKINST}
 
 USE_GMAKE=		Yes
 
+MODULES=		ocaml
+
 CONFIGURE_STYLE=	simple
-## ## add -opt option if there is ocamlc.opt.
-## CONFIGURE_ARGS=		-prefix ${PREFIX} \
-## 			-emacslib ${PREFIX}/share/emacs/site-lisp ## -opt
-## -byteonly for architectures without Ocaml native-code compiler.
 CONFIGURE_ARGS=		-prefix ${PREFIX} \
-			-emacslib ${PREFIX}/share/emacs/site-lisp -byteonly
+			-emacslib ${PREFIX}/share/emacs/site-lisp \
+			${MODOCAML_NATIVE:S/Yes/-opt/:S/No/-byteonly/}
 
 ALL_TARGET=		world
 REGRESS_TARGET=		check
diff --git a/math/coq/pkg/PFRAG.native b/math/coq/pkg/PFRAG.native
new file mode 100644
index 00000000000..b8aab6a5bce
--- /dev/null
+++ b/math/coq/pkg/PFRAG.native
@@ -0,0 +1,2 @@
+@comment $OpenBSD: PFRAG.native,v 1.1 2002/12/18 09:41:07 sturm Exp $
+bin/coqtop.opt
diff --git a/math/coq/pkg/PLIST b/math/coq/pkg/PLIST
index dbcf6504fb9..4861ec8b2cd 100644
--- a/math/coq/pkg/PLIST
+++ b/math/coq/pkg/PLIST
@@ -1,4 +1,5 @@
-@comment $OpenBSD: PLIST,v 1.2 2002/11/04 21:10:44 naddy Exp $
+@comment $OpenBSD: PLIST,v 1.3 2002/12/18 09:40:07 sturm Exp $
+%%native%%
 bin/coq-interface
 bin/coq-tex
 bin/coq_makefile