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/implicit_quantifiers.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/implicit_quantifiers.mli')

diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 5f4129ae0c..39d0174f99 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -13,7 +13,7 @@ open Glob_term
 open Constrexpr
 open Libnames
 
-val declare_generalizable : Vernacexpr.locality_flag -> Misctypes.lident list option -> unit
+val declare_generalizable : local:bool -> Misctypes.lident list option -> unit
 
 val ids_of_list : Id.t list -> Id.Set.t
 val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t
-- 
cgit v1.2.3