diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-08 03:22:22 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-07 02:55:41 +0200 |
| commit | 1d0eb5d4d6fea88abc29798ee2004b2e27e952c6 (patch) | |
| tree | 24b4e369c4acbe2bb9c9ca79b84fc7ddff34e2d8 /Makefile.build | |
| parent | fee2365f13900b4d4f4b88c986cbbf94403eeefa (diff) | |
[camlpX] Remove camlp4 compat layer.
We remove the camlp4 compatibility layer, and try to clean up
most structures. `parsing/compat` is gone.
We added some documentation to the lexer/parser interfaces that are
often obscured by module includes.
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/Makefile.build b/Makefile.build index 01cc4d878..eeb648ba1 100644 --- a/Makefile.build +++ b/Makefile.build @@ -272,11 +272,10 @@ endif ## Explicit dependencies for grammar stuff -GRAMBASEDEPS := grammar/gramCompat.cmo grammar/q_util.cmi -GRAMCMO := grammar/gramCompat.cmo grammar/q_util.cmo \ +GRAMBASEDEPS := grammar/q_util.cmi +GRAMCMO := grammar/q_util.cmo \ grammar/argextend.cmo grammar/tacextend.cmo grammar/vernacextend.cmo -grammar/q_util.cmi : grammar/gramCompat.cmo grammar/argextend.cmo : $(GRAMBASEDEPS) grammar/q_util.cmo : $(GRAMBASEDEPS) grammar/tacextend.cmo : $(GRAMBASEDEPS) grammar/argextend.cmo |