diff options
| author | msozeau | 2008-07-04 14:38:44 +0000 |
|---|---|---|
| committer | msozeau | 2008-07-04 14:38:44 +0000 |
| commit | ff03e8dd0de507be82e58ed5e8fd902dfd7caf4b (patch) | |
| tree | ede6bccf7f4dbcca84e5aca8a374b444527c1686 /library/impargs.mli | |
| parent | e4b265c5f51fbaf87054d13c036878964a98cfcd (diff) | |
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
Diffstat (limited to 'library/impargs.mli')
| -rw-r--r-- | library/impargs.mli | 3 |
1 files changed, 2 insertions, 1 deletions
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 |