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

---
 library/impargs.mli | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

(limited to 'library/impargs.mli')

diff --git a/library/impargs.mli b/library/impargs.mli
index 9038ca88..1d3a73e9 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -1,16 +1,15 @@
 (************************************************************************)
 (*  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 Names
-open Libnames
+open Globnames
 open Term
 open Environ
-open Nametab
 
 (** {6 Implicit Arguments } *)
 (** Here we store the implicit arguments. Notice that we
@@ -68,7 +67,7 @@ type implicit_explanation =
 type maximal_insertion = bool (** true = maximal contextual insertion *)
 type force_inference = bool (** true = always infer, never turn into evar/subgoal *)
 
-type implicit_status = (identifier * implicit_explanation * 
+type implicit_status = (Id.t * implicit_explanation * 
 			  (maximal_insertion * force_inference)) option
     (** [None] = Not implicit *)
 
@@ -78,7 +77,7 @@ type implicits_list = implicit_side_condition * implicit_status list
 
 val is_status_implicit : implicit_status -> bool
 val is_inferable_implicit : bool -> int -> implicit_status -> bool
-val name_of_implicit : implicit_status -> identifier
+val name_of_implicit : implicit_status -> Id.t
 val maximal_insertion_of : implicit_status -> bool
 val force_inference_of : implicit_status -> bool
 
@@ -87,7 +86,7 @@ val positions_of_implicits : implicits_list -> int list
 (** A [manual_explicitation] is a tuple of a positional or named explicitation with
    maximal insertion, force inference and force usage flags. Forcing usage makes
    the argument implicit even if the automatic inference considers it not inferable. *)
-type manual_explicitation = Topconstr.explicitation * 
+type manual_explicitation = Constrexpr.explicitation *
     (maximal_insertion * force_inference * bool)
 
 type manual_implicits = manual_explicitation list
@@ -95,7 +94,7 @@ type manual_implicits = manual_explicitation list
 val compute_implicits_with_manual : env -> types -> bool ->
   manual_implicits -> implicit_status list
 
-val compute_implicits_names : env -> types -> name list
+val compute_implicits_names : env -> types -> Name.t list
 
 (** {6 Computation of implicits (done using the global environment). } *)
 
@@ -130,6 +129,9 @@ val make_implicits_list : implicit_status list -> implicits_list list
 
 val drop_first_implicits : int -> implicits_list -> implicits_list
 
+val projection_implicits : env -> projection -> implicit_status list -> 
+  implicit_status list
+
 val select_impargs_size : int -> implicits_list list -> implicit_status list
 
 val select_stronger_impargs : implicits_list list -> implicit_status list
@@ -143,3 +145,5 @@ type implicit_discharge_request =
   | ImplInteractive of global_reference * implicits_flags *
       implicit_interactive_request
 
+val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool
+(** Equality on [explicitation]. *)
-- 
cgit v1.2.3