diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-01 00:59:46 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-01 00:59:46 +0200 |
| commit | 114d5f0d0bca9f01d7a5ab3381a9b9ca4291191a (patch) | |
| tree | 3aeacfad3a11279599bf4362f8318eb2d8b62ccd /grammar | |
| parent | 842dfef1d52c739119808ea1dec3509c0cf86435 (diff) | |
| parent | d0a9edabf59a858625d11516cdb230d223a77aeb (diff) | |
Merge branch 'yet-another-makefile-bigbang' into trunk
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 |