diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c699f79351..f4ae5bf676 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1643,7 +1643,7 @@ let drop_notations_pattern looked_for genv = | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c) | None -> raise (InternalizationError (loc,NotAConstructor head)) end - | CPatCstr (qid, Some expl_pl, pl) -> + | CPatCstr (qid, Some expl_pl, pl) -> let g = try Nametab.locate qid with Not_found -> raise (InternalizationError (loc,NotAConstructor qid)) in |