aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
diff options
context:
space:
mode:
Diffstat (limited to 'grammar')
-rw-r--r--grammar/argextend.mlp (renamed from grammar/argextend.ml4)2
-rw-r--r--grammar/gramCompat.mlp (renamed from grammar/gramCompat.ml4)0
-rw-r--r--grammar/q_constr.mlp (renamed from grammar/q_constr.ml4)2
-rw-r--r--grammar/q_util.mlp (renamed from grammar/q_util.ml4)0
-rw-r--r--grammar/tacextend.mlp (renamed from grammar/tacextend.ml4)2
-rw-r--r--grammar/vernacextend.mlp (renamed from grammar/vernacextend.ml4)2
6 files changed, 0 insertions, 8 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.mlp
index 8e06adce9..eaaa7f025 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.mlp
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4deps: "tools/compat5b.cmo" i*)
-
open Q_util
open GramCompat
diff --git a/grammar/gramCompat.ml4 b/grammar/gramCompat.mlp
index 6246da7bb..6246da7bb 100644
--- a/grammar/gramCompat.ml4
+++ b/grammar/gramCompat.mlp
diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.mlp
index af90f5f2a..8e1587ec3 100644
--- a/grammar/q_constr.ml4
+++ b/grammar/q_constr.mlp
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4deps: "tools/compat5b.cmo" i*)
-
open Q_util
open GramCompat
open Pcaml
diff --git a/grammar/q_util.ml4 b/grammar/q_util.mlp
index 2d5c40894..2d5c40894 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.mlp
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.mlp
index ae6d2d18e..ac6a7ac7f 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.mlp
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4deps: "tools/compat5b.cmo" i*)
-
(** Implementation of the TACTIC EXTEND macro. *)
open Q_util
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.mlp
index 215d27dbd..ce0431889 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.mlp
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4deps: "tools/compat5b.cmo" i*)
-
(** Implementation of the VERNAC EXTEND macro. *)
open Q_util