diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-17 11:56:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-17 13:15:51 +0100 |
| commit | 22c1e7c3f1d86902b1abf2d887e0e9bf93ddb60d (patch) | |
| tree | 508ca2ee83eaf05e39921759360edfd6004f7039 | |
| parent | 29f26d380177495a224c3b94d3309a3d23693d8f (diff) | |
Removing dead code in Q_util.
| -rw-r--r-- | grammar/q_util.ml4 | 22 | ||||
| -rw-r--r-- | grammar/q_util.mli | 8 |
2 files changed, 0 insertions, 30 deletions
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index f013e323e..1848bf85f 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -28,16 +28,6 @@ let mlexpr_of_pair m1 m2 (a1,a2) = let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in <:expr< ($e1$, $e2$) >> -let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)= - let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 in - let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in - <:expr< ($e1$, $e2$, $e3$) >> - -let mlexpr_of_quadruple m1 m2 m3 m4 (a1,a2,a3,a4)= - let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 and e4 = m4 a4 in - let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e4) in - <:expr< ($e1$, $e2$, $e3$, $e4$) >> - (* We don't give location for tactic quotation! *) let loc = CompatLoc.ghost @@ -57,18 +47,6 @@ let mlexpr_of_option f = function let mlexpr_of_ident id = <:expr< Names.Id.of_string $str:id$ >> -let mlexpr_of_token = function -| Tok.KEYWORD s -> <:expr< Tok.KEYWORD $mlexpr_of_string s$ >> -| Tok.PATTERNIDENT s -> <:expr< Tok.PATTERNIDENT $mlexpr_of_string s$ >> -| Tok.IDENT s -> <:expr< Tok.IDENT $mlexpr_of_string s$ >> -| Tok.FIELD s -> <:expr< Tok.FIELD $mlexpr_of_string s$ >> -| Tok.INT s -> <:expr< Tok.INT $mlexpr_of_string s$ >> -| Tok.INDEX s -> <:expr< Tok.INDEX $mlexpr_of_string s$ >> -| Tok.STRING s -> <:expr< Tok.STRING $mlexpr_of_string s$ >> -| Tok.LEFTQMARK -> <:expr< Tok.LEFTQMARK >> -| Tok.BULLET s -> <:expr< Tok.BULLET $mlexpr_of_string s$ >> -| Tok.EOI -> <:expr< Tok.EOI >> - let repr_entry e = let entry u = let _ = Pcoq.get_entry u e in diff --git a/grammar/q_util.mli b/grammar/q_util.mli index 90fe1645f..837ec6fb0 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -18,14 +18,6 @@ val mlexpr_of_pair : ('a -> MLast.expr) -> ('b -> MLast.expr) -> 'a * 'b -> MLast.expr -val mlexpr_of_triple : - ('a -> MLast.expr) -> ('b -> MLast.expr) -> ('c -> MLast.expr) - -> 'a * 'b * 'c -> MLast.expr - -val mlexpr_of_quadruple : - ('a -> MLast.expr) -> ('b -> MLast.expr) -> - ('c -> MLast.expr) -> ('d -> MLast.expr) -> 'a * 'b * 'c * 'd -> MLast.expr - val mlexpr_of_bool : bool -> MLast.expr val mlexpr_of_int : int -> MLast.expr |