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

1 files changed, 13 insertions, 1 deletions

diff --git a/toplevel/record.mli b/toplevel/record.mli
index c2c6b72ee7..7799162dfd 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -14,6 +14,7 @@ open Term
 open Sign
 open Vernacexpr
 open Topconstr
+open Impargs
 (*i*)
 
 (* [declare_projections ref name coers params fields] declare projections of
@@ -21,7 +22,18 @@ open Topconstr
    as coercions accordingly to [coers]; it returns the absolute names of projections *)
 
 val declare_projections :
-  inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> bool list -> rel_context -> bool list * constant option list
+  inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
+  bool list -> manual_explicitation list list -> rel_context -> 
+  bool list * constant option list
+
+val declare_structure : identifier -> identifier -> 
+  manual_explicitation list -> rel_context -> (* params *)
+  Term.constr -> (* arity *)
+  Impargs.manual_explicitation list list -> Sign.rel_context -> (* fields *)
+  ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
+  bool -> (* coercion? *)
+  bool list -> (* field coercions *)
+  mutual_inductive
 
 val definition_structure :
   lident with_coercion * local_binder list *