diff options
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 93e6f31c0..de7eca352 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -442,7 +442,7 @@ let interp_prim_token = let rec rcp_of_glob looked_for = function | GVar (loc,id) -> RCPatAtom (loc,Some id) - | GHole (loc,_,_) -> RCPatAtom (loc,None) + | GHole (loc,_,_,_) -> RCPatAtom (loc,None) | GRef (loc,g,_) -> looked_for g; RCPatCstr (loc, g,[],[]) | GApp (loc,GRef (_,g,_),l) -> looked_for g; RCPatCstr (loc, g, List.map (rcp_of_glob looked_for) l,[]) |