aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-05 21:24:26 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-05 21:24:26 +0000
commitb65600bf41beefc695478ee19049b2a84186e7ad (patch)
tree59545836f54b454e268cf3e694da1da53de2f80d
parent9fa2e7e48f3259758a462d8de30cfd66af78c627 (diff)
Nouveau mode de compilation de .ml4
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@805 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--parsing/g_proofs.ml42
1 files changed, 2 insertions, 0 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 3f1087c67..0f0d70f8b 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -1,4 +1,6 @@
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
(* $Id$ *)
open Pcoq