aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/egramcoq.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/egramcoq.ml')
-rw-r--r--parsing/egramcoq.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index f47eb1c09..a0384faf8 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -46,7 +46,7 @@ open Egramml
(** Declare Notations grammar rules *)
let constr_expr_of_name (loc,na) = match na with
- | Anonymous -> CHole (loc,None,None)
+ | Anonymous -> CHole (loc,None,Misctypes.IntroAnonymous,None)
| Name id -> CRef (Ident (loc,id), None)
let cases_pattern_expr_of_name (loc,na) = match na with