Réorganisation de Impargs + mise en place d'une infrastructure

(notatemment des tables de parsing et d'affichage différenciées)
permettant au traducteur de changer les implicites


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3874 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 280 insertions, 223 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 6a4de103b..a094e17ab 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -225,9 +225,14 @@ let rec extern inctx scopes vars r =
 	 | RRef (loc,ref) ->
 	     let subscopes = Symbols.find_arguments_scope ref in
 	     let args = extern_args (extern true) scopes vars args subscopes in
-	     extern_app loc (implicits_of_global ref)
+	     extern_app loc (implicits_of_global_out ref)
                (extern_reference loc vars ref)
 	       args
+	 | RVar (loc,id) -> (* useful for translation of inductive *)
+	     let args = List.map (extern true scopes vars) args in
+	     extern_app loc (implicits_of_global_out (VarRef id))
+	       (Ident (loc,id))
+	       args
 	 | _       -> 
 	     explicitize loc [] (extern inctx scopes vars f)
                (List.map (extern true scopes vars) args))
diff --git a/library/declare.ml b/library/declare.ml
index d5dc01cf5..dc0094951 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -102,7 +102,7 @@ let (in_variable, out_variable) =
 
 let declare_variable_common id obj =
   let oname = add_leaf id (in_variable (id,obj)) in
-  if is_implicit_args() then declare_var_implicits id;
+  declare_var_implicits id;
   oname
 
 (* for initial declaration *)
@@ -186,7 +186,7 @@ let hcons_constant_declaration = function
 let declare_constant id (cd,kind) =
   let cd = hcons_constant_declaration cd in
   let (sp,kn as oname) = add_leaf id (in_constant (ConstantEntry cd,kind)) in
-  if is_implicit_args() then declare_constant_implicits kn;
+  declare_constant_implicits kn;
   Dischargedhypsmap.set_discharged_hyps sp [] ;
   !xml_declare_constant oname;
   oname
@@ -194,7 +194,7 @@ let declare_constant id (cd,kind) =
 (* when coming from discharge *)
 let redeclare_constant id discharged_hyps (cd,kind) =
   let _,kn as oname = add_leaf id (in_constant (GlobalRecipe cd,kind)) in
-  if is_implicit_args() then declare_constant_implicits kn;
+  declare_constant_implicits kn;
   Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps
 
 (* Inductives. *)
@@ -280,7 +280,7 @@ let declare_inductive_common mie =
     | [] -> anomaly "cannot declare an empty list of inductives"
   in
   let oname = add_leaf id (in_inductive mie) in
-  if is_implicit_args() then declare_mib_implicits (snd oname);
+  declare_mib_implicits (snd oname);
   oname
 
 (* for initial declaration *)
diff --git a/library/impargs.ml b/library/impargs.ml
index 27cfed221..9faa5a7f2 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -26,22 +26,62 @@ let implicit_args = ref false
 let strict_implicit_args = ref false
 let contextual_implicit_args = ref false
 
-let make_implicit_args flag = implicit_args := flag
-let is_implicit_args () = !implicit_args
+let implicit_args_out = ref false
+let strict_implicit_args_out = ref true
+let contextual_implicit_args_out = ref false
+
+let make_implicit_args flag =
+  implicit_args := flag;
+  if not !Options.v7_only then implicit_args_out := flag
+
+let make_strict_implicit_args flag =
+  strict_implicit_args := flag;
+  if not !Options.v7_only then strict_implicit_args_out := flag
+
+let make_contextual_implicit_args flag =
+  contextual_implicit_args := flag;
+  if not !Options.v7_only then contextual_implicit_args_out := flag
 
-let with_implicits b f x =
-  let oimplicit = !implicit_args in
+let is_implicit_args () = !implicit_args
+let is_implicit_args_out () = !implicit_args_out
+let is_strict_implicit_args () = !strict_implicit_args
+let is_contextual_implicit_args () = !contextual_implicit_args
+
+type implicits_flags = (bool * bool * bool) * (bool * bool * bool)
+
+let with_implicits ((a,b,c),(d,e,g)) f x =
+  let oa = !implicit_args in
+  let ob = !strict_implicit_args in
+  let oc = !contextual_implicit_args in
+  let od = !implicit_args_out in
+  let oe = !strict_implicit_args_out in
+  let og = !contextual_implicit_args_out in
   try 
-    implicit_args := b;
+    implicit_args := a;
+    strict_implicit_args := b;
+    contextual_implicit_args := c;
+    implicit_args_out := d;
+    strict_implicit_args := e;
+    contextual_implicit_args_out := g;
     let rslt = f x in 
-    implicit_args := oimplicit;
+    implicit_args := oa;
+    strict_implicit_args := ob;
+    contextual_implicit_args := oc;
+    implicit_args_out := od;
+    strict_implicit_args_out := oe;
+    contextual_implicit_args_out := og;
     rslt
   with e -> begin
-    implicit_args := oimplicit;
+    implicit_args := oa;
+    strict_implicit_args := ob;
+    contextual_implicit_args := oc;
+    implicit_args_out := od;
+    strict_implicit_args_out := oe;
+    contextual_implicit_args_out := og;
     raise e
   end
 
-let implicitly f = with_implicits true f
+let implicitly f = with_implicits ((false,false,false),(false,false,false)) f
 
 (*s Computation of implicit arguments *)
 
@@ -166,7 +206,7 @@ let add_free_rels_until strict bound env m pos acc =
 
 (* calcule la liste des arguments implicites *)
 
-let compute_implicits env t =
+let compute_implicits output env t =
   let rec aux env n t =
     let t = whd_betadeltaiota env t in
     match kind_of_term t with
@@ -175,8 +215,13 @@ let compute_implicits env t =
             (aux (push_rel (x,None,a) env) (n+1) b)
       | _ -> 
 	  let v = Array.create n None in
-	  if !contextual_implicit_args then
-	    add_free_rels_until !strict_implicit_args n env t Conclusion v
+	  if (not output & !contextual_implicit_args) or
+	     (output & !contextual_implicit_args_out)
+	  then
+	    add_free_rels_until 
+	      (if output then !strict_implicit_args_out 
+	       else !strict_implicit_args)
+	      n env t Conclusion v
 	  else v
   in 
   match kind_of_term (whd_betadeltaiota env t) with 
@@ -209,19 +254,32 @@ let positions_of_implicits =
     | None::l -> aux (n+1) l
   in aux 1
 
+type strict_flag = bool     (* true = strict *)
+type contextual_flag = bool (* true = contextual *)
+
 type implicits =
-  | Impl_auto of implicits_list
+  | Impl_auto of strict_flag * contextual_flag * implicits_list
   | Impl_manual of implicits_list
   | No_impl
 
-let using_implicits = function
-  | No_impl -> with_implicits false
-  | _ -> with_implicits true
-
-let auto_implicits env ty = Impl_auto (compute_implicits env ty)
+let auto_implicits env ty =
+  let impl = 
+    if !implicit_args then
+      let l = compute_implicits false env ty in
+      Impl_auto (!strict_implicit_args,!contextual_implicit_args,l)
+    else
+      No_impl in
+  if Options.do_translate () then
+    impl, 
+    if !implicit_args_out then 
+      (let l = compute_implicits false env ty in
+      Impl_auto (!strict_implicit_args_out,!contextual_implicit_args_out,l))
+    else No_impl
+  else 
+    impl, impl
 
 let list_of_implicits = function 
-  | Impl_auto l -> l
+  | Impl_auto (_,_,l) -> l
   | Impl_manual l -> l
   | No_impl -> []
 
@@ -234,31 +292,8 @@ let compute_constant_implicits kn =
   let cb = lookup_constant kn env in
   auto_implicits env (body_of_type cb.const_type)
 
-let cache_constant_implicits (_,(kn,imps)) = 
-  constants_table := KNmap.add kn imps !constants_table
-
-let subst_constant_implicits (_,subst,(kn,imps as obj)) = 
-  let kn' = subst_kn subst kn in
-    if kn' == kn then obj else
-      kn',imps
-
-let (in_constant_implicits, _) =
-  declare_object {(default_object "CONSTANT-IMPLICITS") with
-    cache_function = cache_constant_implicits;
-    load_function = (fun _ -> cache_constant_implicits);
-    subst_function = subst_constant_implicits;
-    classify_function = (fun (_,x) -> Substitute x);
-    export_function = (fun x -> Some x) }
-
-let declare_constant_implicits kn =
-  let imps = compute_constant_implicits kn in
-  add_anonymous_leaf (in_constant_implicits (kn,imps))
-
 let constant_implicits sp =
-  try KNmap.find sp !constants_table with Not_found -> No_impl
-
-let constant_implicits_list sp =
-  list_of_implicits (constant_implicits sp)
+  try KNmap.find sp !constants_table with Not_found -> No_impl,No_impl
 
 (*s Inductives and constructors. Their implicit arguments are stored
    in an array, indexed by the inductive number, of pairs $(i,v)$ where
@@ -287,40 +322,6 @@ let inductives_table = ref Indmap.empty
 
 let constructors_table = ref Constrmap.empty
 
-let cache_inductive_implicits (_,(indp,imps)) =
-  inductives_table := Indmap.add indp imps !inductives_table
-
-let subst_inductive_implicits (_,subst,((kn,i),imps as obj)) = 
-  let kn' = subst_kn subst kn in
-    if kn' == kn then obj else
-      (kn',i),imps
-
-let (in_inductive_implicits, _) =
-  declare_object {(default_object "INDUCTIVE-IMPLICITS") with 
-    cache_function = cache_inductive_implicits;
-    load_function = (fun _ -> cache_inductive_implicits);
-    subst_function = subst_inductive_implicits;
-    classify_function = (fun (_,x) -> Substitute x);
-    export_function = (fun x -> Some x)  }
-
-let cache_constructor_implicits (_,(consp,imps)) =
-  constructors_table := Constrmap.add consp imps !constructors_table
-
-let subst_constructor_implicits (_,subst,(((kn,i),j),imps as obj)) = 
-  let kn' = subst_kn subst kn in
-    if kn' == kn then obj else
-      ((kn',i),j),imps
-
-
-let (in_constructor_implicits, _) =
-  declare_object {(default_object "CONSTRUCTOR-IMPLICITS") with 
-    cache_function = cache_constructor_implicits;
-    load_function = (fun _ -> cache_constructor_implicits);
-    subst_function = subst_constructor_implicits;
-    classify_function = (fun (_,x) -> Substitute x);
-    export_function = (fun x -> Some x)  }
-
-
 let compute_mib_implicits kn =
   let env = Global.env () in
   let mib = lookup_mind kn env in
@@ -330,53 +331,19 @@ let compute_mib_implicits kn =
         (fun mip -> (Name mip.mind_typename, None, mip.mind_user_arity))
         mib.mind_packets) in
   let env_ar = push_rel_context ar env in
-  let imps_one_inductive mip =
-    (auto_implicits env (body_of_type mip.mind_user_arity),
-     Array.map (fun c -> auto_implicits env_ar (body_of_type c))
+  let imps_one_inductive i mip =
+    let ind = (kn,i) in
+    ((IndRef ind,auto_implicits env (body_of_type mip.mind_user_arity)),
+     Array.mapi (fun j c -> (ConstructRef (ind,j+1),auto_implicits env_ar c))
        mip.mind_user_lc)
   in
-  Array.map imps_one_inductive mib.mind_packets
-
-let cache_mib_implicits (_,(kn,mibimps)) =
-  Array.iteri
-    (fun i (imps,v) ->
-       let indp = (kn,i) in
-       inductives_table := Indmap.add indp imps !inductives_table;
-       Array.iteri 
-	 (fun j imps ->
-	    constructors_table := 
-	      Constrmap.add (indp,succ j) imps !constructors_table) v)
-    mibimps
-
-let subst_mib_implicits (_,subst,(kn,mibimps as obj)) = 
-  let kn' = subst_kn subst kn in
-    if kn' == kn then obj else
-      kn',mibimps
-
-let (in_mib_implicits, _) =
-  declare_object {(default_object "MIB-IMPLICITS") with 
-    cache_function = cache_mib_implicits;
-    load_function = (fun _ -> cache_mib_implicits);
-    subst_function = subst_mib_implicits;
-    classify_function = (fun (_,x) -> Substitute x);
-    export_function = (fun x -> Some x)  }
- 
-let declare_mib_implicits kn =
-  let imps = compute_mib_implicits kn in
-  add_anonymous_leaf (in_mib_implicits (kn,imps))
+  Array.mapi imps_one_inductive mib.mind_packets
 
 let inductive_implicits indp =
-  try Indmap.find indp !inductives_table with Not_found -> No_impl
+  try Indmap.find indp !inductives_table with Not_found -> No_impl,No_impl
 
 let constructor_implicits consp =
-  try Constrmap.find consp !constructors_table with Not_found -> No_impl
-
-let constructor_implicits_list constr_sp = 
-  list_of_implicits (constructor_implicits constr_sp)
-
-let inductive_implicits_list ind_sp =
-  list_of_implicits (inductive_implicits ind_sp)
-
+  try Constrmap.find consp !constructors_table with Not_found -> No_impl,No_impl
 (*s Variables. *)
 
 let var_table = ref Idmap.empty
@@ -386,45 +353,97 @@ let compute_var_implicits id =
   let (_,_,ty) = lookup_named id env in
   auto_implicits env ty
 
-let cache_var_implicits (_,(id,imps)) =
-  var_table := Idmap.add id imps !var_table
+let var_implicits id = 
+  try Idmap.find id !var_table with Not_found -> No_impl,No_impl
+
+(* Caching implicits *)
+
+let cache_implicits_decl (r,imps) =
+  match r with
+  | VarRef id -> 
+      var_table := Idmap.add id imps !var_table
+  | ConstRef kn ->
+      constants_table := KNmap.add kn imps !constants_table
+  | IndRef indp ->
+      inductives_table := Indmap.add indp imps !inductives_table;
+  | ConstructRef consp -> 
+      constructors_table := Constrmap.add consp imps !constructors_table
+
+let cache_implicits (_,l) = List.iter cache_implicits_decl l
+
+let subst_implicits_decl subst (r,imps as o) =
+  let r' = subst_global subst r in if r==r' then o else (r',imps)
+
+let subst_implicits (_,subst,l) =
+  list_smartmap (subst_implicits_decl subst) l
+
+let (in_implicits, _) =
+  declare_object {(default_object "IMPLICITS") with 
+    cache_function = cache_implicits;
+    load_function = (fun _ -> cache_implicits);
+    subst_function = subst_implicits;
+    classify_function = (fun (_,x) -> Substitute x);
+    export_function = (fun x -> Some x) }
+
+(* Implicits of a global reference. *)
 
-let (in_var_implicits, _) =
-  declare_object {(default_object "VARIABLE-IMPLICITS") with 
-    cache_function = cache_var_implicits;
-    load_function = (fun _ -> cache_var_implicits);
-    export_function = (fun x -> Some x)  }
+let compute_global_implicits = function
+  | VarRef id -> compute_var_implicits id
+  | ConstRef kn -> compute_constant_implicits kn
+  | IndRef (kn,i) -> 
+      let ((_,imps),_) = (compute_mib_implicits kn).(i) in imps
+  | ConstructRef ((kn,i),j) -> 
+      let (_,cimps) = (compute_mib_implicits kn).(i) in snd cimps.(j-1)
 
+let declare_implicits_gen r = 
+  add_anonymous_leaf (in_implicits [r,compute_global_implicits r])
 
+let declare_implicits r =
+  with_implicits
+    ((true,!strict_implicit_args,!contextual_implicit_args),
+     (true,!strict_implicit_args_out,!contextual_implicit_args_out))
+    declare_implicits_gen r
 
 let declare_var_implicits id =
-  let imps = compute_var_implicits id in
-  add_anonymous_leaf (in_var_implicits (id,imps))
+  if !implicit_args or !implicit_args_out then
+    declare_implicits_gen (VarRef id)
+
+(* For translator *)
+let set_var_implicits id impls = 
+  add_anonymous_leaf
+    (in_implicits 
+      [VarRef id,
+       (Impl_auto 
+	(!strict_implicit_args,!contextual_implicit_args,impls),
+       Impl_auto 
+	(!strict_implicit_args_out,!contextual_implicit_args_out,impls))])
 
-let implicits_of_var id =
-  list_of_implicits (try Idmap.find id !var_table with Not_found -> No_impl)
+let declare_constant_implicits kn =
+  if !implicit_args or !implicit_args_out then
+    declare_implicits_gen (ConstRef kn)
 
-(*s Implicits of a global reference. *)
+let declare_mib_implicits kn =
+  if !implicit_args or !implicit_args_out then
+  let imps = compute_mib_implicits kn in
+  let imps = array_map_to_list
+    (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) imps in
+  add_anonymous_leaf (in_implicits (List.flatten imps))
 
-let declare_implicits = function
-  | VarRef id -> 
-      declare_var_implicits id
-  | ConstRef kn -> 
-      declare_constant_implicits kn
-  | IndRef ((kn,i) as indp) -> 
-      let mib_imps = compute_mib_implicits kn in
-      let imps = fst mib_imps.(i) in
-      add_anonymous_leaf (in_inductive_implicits (indp, imps))
-  | ConstructRef (((kn,i),j) as consp) -> 
-      let mib_imps = compute_mib_implicits kn in
-      let imps = (snd mib_imps.(i)).(j-1) in
-      add_anonymous_leaf (in_constructor_implicits (consp, imps))
-
-let context_of_global_reference = function
-  | VarRef sp -> []
-  | ConstRef sp -> (Global.lookup_constant sp).const_hyps
-  | IndRef (sp,_) -> (Global.lookup_mind sp).mind_hyps
-  | ConstructRef ((sp,_),_) -> (Global.lookup_mind sp).mind_hyps
+let implicits_of_global_gen = function
+  | VarRef id -> var_implicits id
+  | ConstRef sp -> constant_implicits sp
+  | IndRef isp -> inductive_implicits isp
+  | ConstructRef csp ->	constructor_implicits csp
+
+let implicits_of_global r =
+  let (imp_in,imp_out) = implicits_of_global_gen r in
+  list_of_implicits imp_in
+
+let implicits_of_global_out r =
+  let (imp_in,imp_out) = implicits_of_global_gen r in
+  list_of_implicits imp_out
+
+(* Declare manual implicits *)
 
 let check_range n i =
   if i<1 or i>n then error ("Bad argument number: "^(string_of_int i))
@@ -438,37 +457,31 @@ let declare_manual_implicits r l =
   let rec aux k = function
     | [] -> if k>n then [] else None :: aux (k+1) []
     | p::l as l' ->
-        if k=p then Some Manual :: aux (k+1) l else None :: aux (k+1) l'
-  in let l = Impl_manual (aux 1 l) in
-  match r with
-  | VarRef id -> 
-      add_anonymous_leaf (in_var_implicits (id,l))
-  | ConstRef sp ->
-      add_anonymous_leaf (in_constant_implicits (sp,l))
-  | IndRef indp ->
-      add_anonymous_leaf (in_inductive_implicits (indp,l))
-  | ConstructRef consp -> 
-      add_anonymous_leaf (in_constructor_implicits (consp,l))
+        if k=p then Some Manual :: aux (k+1) l else None :: aux (k+1) l' in
+  let l = Impl_manual (aux 1 l) in
+  let l = l,l in
+  add_anonymous_leaf (in_implicits [r,l])
 
-(*s Tests if declared implicit *)
+(* Tests if declared implicit *)
 
+let test = function
+  | No_impl | Impl_manual _ -> false,false,false
+  | Impl_auto (s,c,_) -> true,s,c
+
+let test_if_implicit find a =
+  try let b,c = find a in test b, test c
+  with Not_found -> (false,false,false),(false,false,false)
+    
 let is_implicit_constant sp =
-  try let _ = KNmap.find sp !constants_table in true with Not_found -> false
+  test_if_implicit (KNmap.find sp) !constants_table
 
 let is_implicit_inductive_definition indp =
-  try let _ = Indmap.find indp !inductives_table in true 
-  with Not_found -> false
+  test_if_implicit (Indmap.find (indp,0)) !inductives_table
 
 let is_implicit_var id =
-  try let _ = Idmap.find id !var_table in true with Not_found -> false
-
-let implicits_of_global = function
-  | VarRef id -> implicits_of_var id
-  | ConstRef sp -> list_of_implicits (constant_implicits sp)
-  | IndRef isp -> list_of_implicits (inductive_implicits isp)
-  | ConstructRef csp ->	list_of_implicits (constructor_implicits csp)
+  test_if_implicit (Idmap.find id) !var_table
 
-(*s Registration as global tables and rollback. *)
+(*s Registration as global tables *)
 
 type frozen_t = implicits KNmap.t 
               * implicits Indmap.t 
@@ -497,7 +510,3 @@ let _ =
       Summary.unfreeze_function = unfreeze;
       Summary.init_function = init;
       Summary.survive_section = false }
-
-let rollback f x =
-  let fs = freeze () in
-  try f x with e -> begin unfreeze fs; raise e end
diff --git a/library/impargs.mli b/library/impargs.mli
index 09462ea23..a9f57e288 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -20,12 +20,16 @@ open Nametab
     are outside the kernel, which knows nothing about implicit arguments. *)
 
 val make_implicit_args : bool -> unit
+val make_strict_implicit_args : bool -> unit
+val make_contextual_implicit_args : bool -> unit
+
 val is_implicit_args : unit -> bool
-val implicitly : ('a -> 'b) -> 'a -> 'b
-val with_implicits : bool -> ('a -> 'b) -> 'a -> 'b
+val is_strict_implicit_args : unit -> bool
+val is_contextual_implicit_args : unit -> bool
 
-val strict_implicit_args : bool ref
-val contextual_implicit_args : bool ref
+type implicits_flags
+val implicitly : ('a -> 'b) -> 'a -> 'b
+val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b
 
 (*s An [implicits_list] is a list of positions telling which arguments
     of a reference can be automatically infered *)
@@ -38,34 +42,27 @@ val positions_of_implicits : implicits_list -> int list
 
 (* Computation of the positions of arguments automatically inferable
    for an object of the given type in the given env *)
-val compute_implicits : env -> types -> implicits_list
+val compute_implicits : bool -> env -> types -> implicits_list
 
 (*s Computation of implicits (done using the global environment). *)
 
 val declare_var_implicits : variable -> unit
 val declare_constant_implicits : constant -> unit
 val declare_mib_implicits : mutual_inductive -> unit
+
 val declare_implicits : global_reference -> unit
 
 (* Manual declaration of which arguments are expected implicit *)
 val declare_manual_implicits : global_reference -> int list -> unit
 
-(*s Access to already computed implicits. *)
-
-val constructor_implicits_list : constructor -> implicits_list
-val inductive_implicits_list : inductive -> implicits_list
-val constant_implicits_list : constant -> implicits_list
-
-val implicits_of_var : variable -> implicits_list
-
-val is_implicit_constant : constant -> bool
-val is_implicit_inductive_definition : inductive -> bool
-val is_implicit_var : variable -> bool
+(* Get implicit arguments *)
+val is_implicit_constant : constant -> implicits_flags
+val is_implicit_inductive_definition : mutual_inductive -> implicits_flags
+val is_implicit_var : variable -> implicits_flags
 
 val implicits_of_global : global_reference -> implicits_list
 
-(*s Rollback. *)
-
-type frozen_t
-val freeze : unit -> frozen_t
-val unfreeze : frozen_t -> unit
+(* For translator *)
+val implicits_of_global_out : global_reference -> implicits_list
+val is_implicit_args_out : unit -> bool
+val set_var_implicits : variable -> implicits_list -> unit
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 648d4690d..7aa435984 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -83,11 +83,11 @@ let implicit_args_id id l =
 let implicit_args_msg sp mipv = 
   (prvecti
        (fun i mip -> 
-	  let imps = inductive_implicits_list (sp,i) in
+	  let imps = implicits_of_global (IndRef (sp,i)) in
           ((implicit_args_id mip.mind_typename imps) ++
              prvecti 
 	       (fun j idc ->
-		  let imps = constructor_implicits_list ((sp,i),succ j) in
+		  let imps = implicits_of_global (ConstructRef ((sp,i),j+1)) in
                   (implicit_args_id idc imps))
                mip.mind_consnames 
 ))
@@ -153,7 +153,7 @@ let print_mutual sp =
 
 let print_section_variable sp =
   let d = get_variable sp in
-  let l = implicits_of_var sp in
+  let l = implicits_of_global (VarRef sp) in
   (print_named_decl d ++ print_impl_args l)
 
 let print_body = function
@@ -167,7 +167,7 @@ let print_constant with_values sep sp =
   let cb = Global.lookup_constant sp in
   let val_0 = cb.const_body in
   let typ = cb.const_type in
-  let impls = constant_implicits_list sp in
+  let impls = implicits_of_global (ConstRef sp) in
   hov 0 ((match val_0 with 
 		| None -> 
 		    (str"*** [ " ++ 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 63c7cce93..6c33b3783 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -208,7 +208,7 @@ let interp_mutual lparams lnamearconstrs finite =
 	 let env' = Termops.push_rel_assum (Name recname,fullarity) env in
 	 let impls = 
 	   if Impargs.is_implicit_args()
-	   then Impargs.compute_implicits env_params fullarity
+	   then Impargs.compute_implicits false env_params fullarity
 	   else [] in
 	 (env', (recname,impls)::ind_impls, (arity::arl)))
       (env0, [], []) lnamearconstrs
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index f3c4b68b3..1eb74c7e7 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -182,11 +182,11 @@ let inductive_message inds =
 type opacity = bool
 
 type discharge_operation = 
-  | Variable of identifier * section_variable_entry * local_kind * bool *
-      Dischargedhypsmap.discharged_hyps
-  | Constant of identifier * recipe * global_kind * constant * bool * 
-      Dischargedhypsmap.discharged_hyps
-  | Inductive of mutual_inductive_entry * bool *
+  | Variable of identifier * section_variable_entry * local_kind * 
+      implicits_flags * Dischargedhypsmap.discharged_hyps
+  | Constant of identifier * recipe * global_kind * constant * 
+      implicits_flags * Dischargedhypsmap.discharged_hyps
+  | Inductive of mutual_inductive_entry * implicits_flags *
       Dischargedhypsmap.discharged_hyps
   | Class of cl_typ * cl_info_typ
   | Struc of inductive * (unit -> struc_typ)
@@ -234,7 +234,8 @@ let process_object oldenv olddir full_olddir newdir
 	let kn = Nametab.locate_mind (qualid_of_sp sp) in
 	let mib = Environ.lookup_mind kn oldenv in
 	let newkn = recalc_kn newdir kn in
-	let imp = is_implicit_args() (* CHANGE *) in
+	let imp = is_implicit_inductive_definition kn in
+(*	let imp = is_implicit_args (* CHANGE *) in*)
 	let (mie,indmods,cstrmods,discharged_hyps0) = 
 	  process_inductive full_olddir kn newkn oldenv (ids_to_discard,work_alist) mib in
         (* let's add the new discharged hypothesis to those already discharged*)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 6eab9d36e..1269ddfe3 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -140,13 +140,16 @@ let rec vernac_com interpfun (loc,com) =
              Options.v7_only := true;
              if !translate_file then msgnl (pr_comments !comments)
          | _ ->
+	     let f = match com with (* Pour gérer les implicites *)
+	       | VernacInductive _ -> States.with_heavy_rollback
+	       | _ -> fun f -> f in
              if !translate_file then
-	       msgnl
-                 (pr_comments !comments ++ hov 0 (pr_vernac com) ++ sep_end) 
+               msgnl
+		 (pr_comments !comments ++ hov 0 (f pr_vernac com) ++ sep_end)
              else
 	       msgnl
                  (hov 4 (str"New Syntax:" ++ fnl() ++ pr_comments !comments ++
-                         pr_vernac com ++ sep_end)));
+                         f pr_vernac com ++ sep_end)));
        comments := None;
        Format.set_formatter_out_channel stdout);
     interp com;
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 81bcd4735..afd017bed 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -744,16 +744,16 @@ let _ =
     { optsync  = true;
       optname  = "strict implicits";
       optkey   = (SecondaryTable ("Strict","Implicits"));
-      optread  = (fun () -> !Impargs.strict_implicit_args);
-      optwrite = (fun b ->  Impargs.strict_implicit_args := b) }
+      optread  = Impargs.is_strict_implicit_args;
+      optwrite = Impargs.make_strict_implicit_args }
 
 let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "contextual implicits";
       optkey   = (SecondaryTable ("Contextual","Implicits"));
-      optread  = (fun () -> !Impargs.contextual_implicit_args);
-      optwrite = (fun b ->  Impargs.contextual_implicit_args := b) }
+      optread  = Impargs.is_contextual_implicit_args;
+      optwrite = Impargs.make_contextual_implicit_args }
 
 let _ =
   declare_bool_option 
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 76771ece7..dfe934b7b 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -502,6 +502,30 @@ let rec pr_vernac = function
       hov 2
         (pr_assumption_token stre ++ spc() ++ pr_ne_params_list pr_lconstr l)
   | VernacInductive (f,l) ->
+
+      (* Copie simplifiée de command.ml pour recalculer les implicites *)
+      let lparams = match l with [] -> assert false | (_,la,_,_)::_ -> la in
+      let nparams = List.length lparams
+      and sigma = Evd.empty 
+      and env0 = Global.env() in
+      let (env_params,params) =
+	List.fold_left
+	  (fun (env,params) (id,t) ->
+	    let p = Constrintern.interp_binder sigma env (Name id) t in
+	    (Termops.push_rel_assum (Name id,p) env,
+	    (Name id,None,p)::params))
+	  (env0,[]) lparams in
+      List.iter
+	(fun (recname, _,arityc,_) ->
+	  let arity = Constrintern.interp_type sigma env_params arityc in
+	  let fullarity =
+            Termops.prod_it arity (List.map (fun (id,_,ty) -> (id,ty)) params) in
+	  if Impargs.is_implicit_args_out()
+	  then
+	    Impargs.set_var_implicits recname
+	      (Impargs.compute_implicits false env_params fullarity)) l;
+      (* Fin calcul implicites *)
+
       let pr_constructor (coe,(id,c)) =
         hov 2 (pr_id id ++ str" " ++
                (if coe then str":>" else str":") ++
@@ -514,10 +538,26 @@ let rec pr_vernac = function
       let pr_oneind (id,indpar,s,lc) =
         pr_id id ++ spc() ++ pr_sbinders indpar ++ str":" ++ spc() ++
         pr_lconstr s ++ str" :=" ++ pr_constructor_list lc in
+      let p = prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_oneind l in
       hov 1
-        ((if f then str"Inductive" else str"CoInductive") ++ spc() ++
-        prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_oneind l)
+        ((if f then str"Inductive" else str"CoInductive") ++ spc() ++ p)
+
   | VernacFixpoint recs ->
+
+      (* Copie simplifiée de command.ml pour recalculer les implicites *)
+      let sigma = Evd.empty
+      and env0 = Global.env() in
+      let fs = States.freeze() in
+      (try 
+	List.iter
+          (fun (recname,_,arityc,_) -> 
+            let arity = Constrintern.interp_type sigma env0 arityc in
+            let _ = Declare.declare_variable recname
+	      (Lib.cwd(),Declare.SectionLocalAssum arity, Decl_kinds.IsAssumption Decl_kinds.Definitional) in ())
+          recs
+      with e ->
+	States.unfreeze fs; raise e);
+
       let pr_onerec = function
         | (id,n,type_0,def0) ->
             let (bl,def,type_) = extract_def_binders def0 type_0 in
@@ -534,8 +574,10 @@ let rec pr_vernac = function
             pr_id id ++ str" " ++ pr_binders bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr c) type_
             ++ str" :=" ++ brk(1,1) ++ pr_lconstr def in
-      hov 1 (str"Fixpoint" ++ spc() ++
-      prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs)  
+      let p = prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs in
+      States.unfreeze fs;
+      hov 1 (str"Fixpoint" ++ spc() ++ p)
+
   | VernacCoFixpoint corecs ->
       let pr_onecorec (id,c,def) =
         let (bl,def,c) = extract_def_binders def c in