From b4b515c2e61bc6ea662b48e84eb319ec8252b07d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 19 May 2018 16:54:01 +0200
Subject: [api] Move `Vernacexpr` to parsing.

There were a few spurious dependencies on the `Vernac` AST in the
pretyper, we remove them and move `Vernacexpr` and `Extend` to parsing,
where they do belong more.
---
 interp/dumpglob.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/dumpglob.ml')

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index bc6a1ef3aa..74618a2905 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -254,7 +254,7 @@ let dump_def ?loc ty secpath id = Option.iter (fun loc ->
 let dump_definition {CAst.loc;v=id} sec s =
   dump_def ?loc s (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id)
 
-let dump_constraint (({ CAst.loc; v = n },_), _, _) sec ty =
+let dump_constraint { CAst.loc; v = n } sec ty =
   match n with
     | Names.Name id -> dump_definition CAst.(make ?loc id) sec ty
     | Names.Anonymous -> ()
-- 
cgit v1.2.3