From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- interp/impargs.mli | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'interp/impargs.mli') diff --git a/interp/impargs.mli b/interp/impargs.mli index 103a4f9e..ea5aa90f 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -10,7 +10,6 @@ open Names open EConstr -open Globnames open Environ (** {6 Implicit Arguments } *) @@ -103,7 +102,7 @@ val declare_var_implicits : variable -> unit val declare_constant_implicits : Constant.t -> unit val declare_mib_implicits : MutInd.t -> unit -val declare_implicits : bool -> global_reference -> unit +val declare_implicits : bool -> GlobRef.t -> unit (** [declare_manual_implicits local ref enriching l] Manual declaration of which arguments are expected implicit. @@ -111,15 +110,15 @@ val declare_implicits : bool -> global_reference -> unit implicits depending on the current state. Unsets implicits if [l] is empty. *) -val declare_manual_implicits : bool -> global_reference -> ?enriching:bool -> +val declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool -> manual_implicits list -> unit (** If the list is empty, do nothing, otherwise declare the implicits. *) -val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool -> +val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool -> manual_implicits -> unit -val implicits_of_global : global_reference -> implicits_list list +val implicits_of_global : GlobRef.t -> implicits_list list val extract_impargs_data : implicits_list list -> ((int * int) option * implicit_status list) list -- cgit v1.2.3