aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/egrammar.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/egrammar.ml')
-rw-r--r--parsing/egrammar.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index c3b5d98f8..83f4cad58 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -281,7 +281,8 @@ let subst_constr_expr a loc subs =
| CCast (_,a,b) -> CCast (loc,subst a,subst b)
| CNotation (_,n,l) -> CNotation (loc,n,List.map subst l)
| CDelimiters (_,s,a) -> CDelimiters (loc,s,subst a)
- | CHole _ | CMeta _ | CSort _ | CNumeral _ | CDynamic _ | CRef _ as x -> x
+ | CHole _ | CEvar _ | CPatVar _ | CSort _
+ | CNumeral _ | CDynamic _ | CRef _ as x -> x
| CCases (_,po,a,bl) ->
(* TODO: apply g on the binding variables in pat... *)
let bl = List.map (fun (_,pat,rhs) -> (loc,pat,subst rhs)) bl in