aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_prim.ml4
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2017-03-08 03:22:22 +0100
committerEmilio Jesus Gallego Arias2017-04-07 02:55:41 +0200
commit1d0eb5d4d6fea88abc29798ee2004b2e27e952c6 (patch)
tree24b4e369c4acbe2bb9c9ca79b84fc7ddff34e2d8 /parsing/g_prim.ml4
parentfee2365f13900b4d4f4b88c986cbbf94403eeefa (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 'parsing/g_prim.ml4')
-rw-r--r--parsing/g_prim.ml41
1 files changed, 0 insertions, 1 deletions
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 2db91b8f87..2af4ed533b 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Compat
open Names
open Libnames
open Tok (* necessary for camlp4 *)