diff options
| author | Pierre-Marie Pédrot | 2014-07-25 20:22:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-07-25 20:24:49 +0200 |
| commit | 0736cd1ff1eb07c6faae43cdfbe2efd11c8470e9 (patch) | |
| tree | ecb06e9072845622a0b1b0d5c447064ae8f630b8 /grammar | |
| parent | 8aec3a45d93b61874ef2567d1430821067905eb3 (diff) | |
Removing dead code relative to or_metaid.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/q_coqast.ml4 | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index 360b96dc4a..d1f4587915 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -71,10 +71,6 @@ let mlexpr_of_intro_pattern = function let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident) -let mlexpr_of_or_metaid f = function - | Tacexpr.AI a -> <:expr< Tacexpr.AI $f a$ >> - | Tacexpr.MetaId (_,id) -> <:expr< Tacexpr.AI $anti loc id$ >> - let mlexpr_of_quantified_hypothesis = function | Misctypes.AnonHyp n -> <:expr< Glob_term.AnonHyp $mlexpr_of_int n$ >> | Misctypes.NamedHyp id -> <:expr< Glob_term.NamedHyp $mlexpr_of_ident id$ >> |