From a086919e4bab3fba4469d7374851a2d95021f528 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 12:50:51 +0100
Subject: Minor indentation change.

---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3