aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/egramcoq.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/egramcoq.ml')
-rw-r--r--parsing/egramcoq.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 3245c642f..e2b78d725 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -47,7 +47,7 @@ open Egramml
let constr_expr_of_name (loc,na) = match na with
| Anonymous -> CHole (loc,None,None)
- | Name id -> CRef (Ident (loc,id))
+ | Name id -> CRef (Ident (loc,id), None)
let cases_pattern_expr_of_name (loc,na) = match na with
| Anonymous -> CPatAtom (loc,None)
@@ -76,7 +76,7 @@ let make_constr_action
make (v :: constrs, constrlists, binders) tl)
| ETReference ->
Gram.action (fun (v:reference) ->
- make (CRef v :: constrs, constrlists, binders) tl)
+ make (CRef (v,None) :: constrs, constrlists, binders) tl)
| ETName ->
Gram.action (fun (na:Loc.t * Name.t) ->
make (constr_expr_of_name na :: constrs, constrlists, binders) tl)