From ff03e8dd0de507be82e58ed5e8fd902dfd7caf4b Mon Sep 17 00:00:00 2001 From: msozeau Date: Fri, 4 Jul 2008 14:38:44 +0000 Subject: Fixes in handling of implicit arguments: - Now [ id : Class foo ] makes id an explicit argument, and [ Class foo ] is equivalent to [ {someid} : Class foo ]. This makes declarations such as "Class Ord [ eq : Eq a ]" have sensible implicit args. - Better handling of {} in class and record declarations, refactorize code for declaring structures and classes. - Fix merging of implicit arguments information on section closing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11204 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/impargs.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'library/impargs.mli') diff --git a/library/impargs.mli b/library/impargs.mli index 1206600273..5bfa0470d3 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -47,7 +47,6 @@ val is_status_implicit : implicit_status -> bool val is_inferable_implicit : bool -> int -> implicit_status -> bool val name_of_implicit : implicit_status -> identifier val maximal_insertion_of : implicit_status -> bool -val forced_implicit : implicit_status -> bool val positions_of_implicits : implicits_list -> int list @@ -83,3 +82,5 @@ val maybe_declare_manual_implicits : bool -> global_reference -> bool -> manual_explicitation list -> unit val implicits_of_global : global_reference -> implicits_list + +val lift_implicits : int -> manual_explicitation list -> manual_explicitation list -- cgit v1.2.3