From 82663b28a04d82e89bd041efd256c4838312e587 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 23 May 2019 10:03:42 +0200
Subject: Simplify implicit_quantifiers

After removing `Instance : !type` implicit_application is only used in
constrintern. We propagate constant arguments ?allow_partial and
combine_params_freevar.

Also remove unused functions.
---
 interp/implicit_quantifiers.mli | 17 +----------------
 1 file changed, 1 insertion(+), 16 deletions(-)

(limited to 'interp/implicit_quantifiers.mli')

diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 437fef1753..d28d35f3a1 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -11,22 +11,14 @@
 open Names
 open Glob_term
 open Constrexpr
-open Libnames
 
 val declare_generalizable : local:bool -> lident list option -> unit
 
-val ids_of_list : Id.t list -> Id.Set.t
-val destClassApp : constr_expr -> (qualid * constr_expr list * instance_expr option) CAst.t
-val destClassAppExpl : constr_expr -> (qualid * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t
-
 (** Fragile, should be used only for construction a set of identifiers to avoid *)
 
 val free_vars_of_constr_expr : constr_expr -> ?bound:Id.Set.t ->
   Id.t list -> Id.t list
 
-val free_vars_of_binders :
-  ?bound:Id.Set.t -> Id.t list -> local_binder_expr list -> Id.Set.t * Id.t list
-
 (** Returns the generalizable free ids in left-to-right
    order with the location of their first occurrence *)
 
@@ -37,14 +29,7 @@ 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 :
-  Id.Set.t -> GlobRef.t option * Constr.rel_declaration ->
-  Constrexpr.constr_expr * Id.Set.t
-
-val implicit_application : Id.Set.t -> ?allow_partial:bool ->
-  (Id.Set.t -> GlobRef.t option * Constr.rel_declaration ->
-    Constrexpr.constr_expr * Id.Set.t) ->
-  constr_expr -> constr_expr * Id.Set.t
+val implicit_application : Id.Set.t -> constr_expr -> constr_expr * Id.Set.t
 
 (* Should be likely located elsewhere *)
 exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *)
-- 
cgit v1.2.3