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 /grammar/q_util.mlp | |
| 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 'grammar/q_util.mlp')
| -rw-r--r-- | grammar/q_util.mlp | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp index 0dd096ef7..8b930cf36 100644 --- a/grammar/q_util.mlp +++ b/grammar/q_util.mlp @@ -8,8 +8,6 @@ (* This file defines standard combinators to build ml expressions *) -open GramCompat - type argument_type = | ListArgType of argument_type | OptArgType of argument_type @@ -33,17 +31,17 @@ let mlexpr_of_list f l = List.fold_right (fun e1 e2 -> let e1 = f e1 in - let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in + let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in <:expr< [$e1$ :: $e2$] >>) - l (let loc = CompatLoc.ghost in <:expr< [] >>) + l (let loc = Ploc.dummy in <:expr< [] >>) let mlexpr_of_pair m1 m2 (a1,a2) = let e1 = m1 a1 and e2 = m2 a2 in - let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in + let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in <:expr< ($e1$, $e2$) >> (* We don't give location for tactic quotation! *) -let loc = CompatLoc.ghost +let loc = Ploc.dummy let mlexpr_of_bool = function |