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, 0 insertions, 7 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index df133e7693..14e64ead46 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -613,13 +613,6 @@ let _ =
       optread  = (fun () -> !elim_flag) ;
       optwrite = (fun b -> elim_flag := b) }
 
-
-let lift_implicits n = 
-  List.map (fun x -> 
-    match fst x with 
-	ExplByPos (k, id) -> ExplByPos (k + n, id), snd x
-      | _ -> x)
-
 let declare_mutual_with_eliminations isrecord mie impls =
   let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
   let params = List.length mie.mind_entry_params in