aboutsummaryrefslogtreecommitdiff
path: root/grammar
diff options
context:
space:
mode:
Diffstat (limited to 'grammar')
-rw-r--r--grammar/q_coqast.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index a52fdeb62c..cada607f67 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -83,7 +83,7 @@ let mlexpr_of_or_var f = function
| Misctypes.ArgArg x -> <:expr< Misctypes.ArgArg $f x$ >>
| Misctypes.ArgVar id -> <:expr< Misctypes.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >>
-let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident)
+let mlexpr_of_hyp = (mlexpr_of_located mlexpr_of_ident)
let mlexpr_of_occs = function
| Locus.AllOccurrences -> <:expr< Locus.AllOccurrences >>