From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 interp/implicit_quantifiers.mli | 47 ++++++++++++++++++-----------------------
 1 file changed, 20 insertions(+), 27 deletions(-)

(limited to 'interp/implicit_quantifiers.mli')

diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index ab2ad566..818f7e9a 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -1,54 +1,47 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Names
-open Decl_kinds
-open Term
-open Sign
-open Evd
-open Environ
-open Nametab
-open Mod_subst
 open Glob_term
-open Topconstr
-open Util
+open Constrexpr
 open Libnames
-open Typeclasses
+open Globnames
 
-val declare_generalizable : Vernacexpr.locality_flag -> (identifier located) list option -> unit
+val declare_generalizable : Vernacexpr.locality_flag -> (Id.t located) list option -> unit
 
-val ids_of_list : identifier list -> Idset.t
-val destClassApp : constr_expr -> loc * reference * constr_expr list
-val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list
+val ids_of_list : Id.t list -> Id.Set.t
+val destClassApp : constr_expr -> Loc.t * reference * constr_expr list
+val destClassAppExpl : constr_expr -> Loc.t * reference * (constr_expr * explicitation located option) list
 
 (** Fragile, should be used only for construction a set of identifiers to avoid *)
 
-val free_vars_of_constr_expr : constr_expr -> ?bound:Idset.t ->
-  identifier list -> identifier list
+val free_vars_of_constr_expr : constr_expr -> ?bound:Id.Set.t ->
+  Id.t list -> Id.t list
 
 val free_vars_of_binders :
-  ?bound:Idset.t -> Names.identifier list -> local_binder list -> Idset.t * Names.identifier list
+  ?bound:Id.Set.t -> Id.t list -> local_binder list -> Id.Set.t * Id.t list
 
 (** Returns the generalizable free ids in left-to-right
    order with the location of their first occurence *)
 
-val generalizable_vars_of_glob_constr : ?bound:Idset.t -> ?allowed:Idset.t ->
-  glob_constr -> (Names.identifier * loc) list
+val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t ->
+  glob_constr -> (Id.t * Loc.t) list
 
-val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
+val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
 
 val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
 
 val combine_params_freevar :
-  Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
-  Topconstr.constr_expr * Names.Idset.t
+  Id.Set.t -> (global_reference * bool) option * (Name.t * Term.constr option * Term.types) ->
+  Constrexpr.constr_expr * Id.Set.t
 
-val implicit_application : Idset.t -> ?allow_partial:bool ->
-  (Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
-    Topconstr.constr_expr * Names.Idset.t) ->
-  constr_expr -> constr_expr * Idset.t
+val implicit_application : Id.Set.t -> ?allow_partial:bool ->
+  (Id.Set.t -> (global_reference * bool) option * (Name.t * Term.constr option * Term.types) ->
+    Constrexpr.constr_expr * Id.Set.t) ->
+  constr_expr -> constr_expr * Id.Set.t
-- 
cgit v1.2.3