diff options
| author | Hugo Herbelin | 2019-11-14 12:50:51 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-01-30 18:59:26 +0100 |
| commit | a086919e4bab3fba4469d7374851a2d95021f528 (patch) | |
| tree | 59972639ab26a2291cd63d951306a9b5fa3c760f | |
| parent | a71fa32802d05bfe63263730c40e93015bb71f8b (diff) | |
Minor indentation change.
| -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 |