Nouveaux changements autour des implicites (notamment suite Ã

discussion avec Georges)

- La notion d'insertion maximale n'est plus globale mais attachée à
  chaque implicite
- Correction de petits bugs dans le calcul des implicites
- Raffinement de la notion "sous contexte" pour l'affichage des coercions



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

14 files changed, 160 insertions, 110 deletions

diff --git a/CHANGES b/CHANGES
index 14e9b64170..ea73490d76 100644
--- a/CHANGES
+++ b/CHANGES
@@ -15,8 +15,13 @@ Libraries
   incompatibilities].
 - Boolean operators moved from module Bool to module Datatypes.
 
-Notations
+Notations and implicit arguments
 
+- New options "Set Maximal Implicit Insertion", "Set Reversible Pattern
+  Implicit", "Set Strongly Strict Implicit" and "Set Printing Implicit
+  Defensive" for controlling inference and use of implicit arguments.
+- New modifier in "Implicit Arguments" to force an implicit argument to
+  be maximally inserted.
 - Level "constr" moved from 9 to 8.
 
 Tactic Language
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 0101b10967..2abdcaa19c 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -2079,10 +2079,10 @@ let rec xlate_vernac =
 	       CT_coerce_ID_LIST_to_ID_LIST_OPT
 	       (CT_id_list
 	       (List.map
-		  (function ExplByPos x
+		  (function ExplByPos x, _
 		       -> xlate_error
 			   "explication argument by rank is obsolete"
-		     | ExplByName id -> CT_ident (string_of_id id)) l)))
+		     | ExplByName id, _ -> CT_ident (string_of_id id)) l)))
   | VernacDeclareImplicits(false, id, opt_positions) ->
       xlate_error "TODO: Implicit Arguments Global"
   | VernacReserve((_,a)::l, f) ->
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 537978269c..771a0b299d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -563,16 +563,17 @@ let rec extern_args extern scopes env args subscopes =
 
 let rec remove_coercions inctx = function
   | RApp (loc,RRef (_,r),args) as c
-      when inctx & not (!Options.raw_print or !print_coercions)
+      when  not (!Options.raw_print or !print_coercions)
       ->
+      let nargs = List.length args in
       (try match Classops.hide_coercion r with
-	  | Some n when n < List.length args ->
+	  | Some n when n < nargs && (inctx or n+1 < nargs) ->
 	      (* We skip a coercion *) 
 	      let l = list_skipn n args in
-              let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
-              let (a,l) =
+	      let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
+	      let (a,l) =
                 (* Recursively remove the head coercions *)
-                match remove_coercions inctx a with
+                match remove_coercions true a with
                   | RApp (_,a,l') -> a,l'@l
                   | a -> a,l in
               if l = [] then a
@@ -886,7 +887,7 @@ let extern_constr_gen at_top scopt env t =
   let avoid = if at_top then ids_of_context env else [] in
   let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
   let vars = vars_of_env env in
-  extern (not at_top) (scopt,[]) vars r
+  extern false (scopt,[]) vars r
 
 let extern_constr_in_scope at_top scope env t =
   extern_constr_gen at_top (Some scope) env t
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 9b3268930c..f5ad4172c1 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -44,8 +44,6 @@ let for_grammar f x =
 
 let variables_bind = ref false
 
-let insert_maximal_implicit = ref false
-
 (**********************************************************************)
 (* Internalisation errors                                             *)
 
@@ -1035,10 +1033,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	    let eargs' = List.remove_assoc id eargs in
 	    intern enva a :: aux (n+1) impl' subscopes' eargs' rargs
 	  with Not_found ->
-	  if rargs=[] & eargs=[] & not !insert_maximal_implicit &
-	    not (List.for_all is_status_implicit impl') then
-	    (* Less regular arguments than expected: don't complete *)
-	    (* with implicit arguments *)
+	  if rargs=[] & eargs=[] & not (maximal_insertion_of imp) then
+            (* Less regular arguments than expected: complete *)
+            (* with implicit arguments if maximal insertion is set *)
 	    []
 	  else
 	    RHole (set_hole_implicit (n,get_implicit_name n l) c) :: 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index d7634d6e09..edbf9fb62a 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -47,8 +47,6 @@ type full_implicits_env = identifier list * implicits_env
 
 type ltac_sign = identifier list * unbound_ltac_var_map
 
-val insert_maximal_implicit : bool ref
-
 (*s Internalisation performs interpretation of global names and notations *)
 
 val intern_constr : evar_map -> env -> constr_expr -> rawconstr
diff --git a/library/impargs.ml b/library/impargs.ml
index 2caf4d1108..52ea66de0c 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -27,10 +27,11 @@ open Topconstr
 
 type implicits_flags = {
   main : bool;
-  strict : bool;
-  strong_strict : bool;
+  strict : bool;                   (* true = strict *)
+  strongly_strict : bool;            (* true = strongly strict *)
   reversible_pattern : bool;
-  contextual : bool
+  contextual : bool;               (* true = contextual *)
+  maximal : bool
 }
 
 (* les implicites sont stricts par défaut en v8 *)
@@ -38,9 +39,10 @@ type implicits_flags = {
 let implicit_args = ref { 
   main = false;
   strict = true;
-  strong_strict = false;
+  strongly_strict = false;
   reversible_pattern = false;
-  contextual = false
+  contextual = false;
+  maximal = false;
 }
 
 let make_implicit_args flag =
@@ -49,8 +51,8 @@ let make_implicit_args flag =
 let make_strict_implicit_args flag =
   implicit_args := { !implicit_args with strict = flag }
 
-let make_strong_strict_implicit_args flag =
-  implicit_args := { !implicit_args with strong_strict = flag }
+let make_strongly_strict_implicit_args flag =
+  implicit_args := { !implicit_args with strongly_strict = flag }
 
 let make_reversible_pattern_implicit_args flag =
   implicit_args := { !implicit_args with reversible_pattern = flag }
@@ -58,11 +60,15 @@ let make_reversible_pattern_implicit_args flag =
 let make_contextual_implicit_args flag =
   implicit_args := { !implicit_args with contextual = flag }
 
+let make_maximal_implicit_args flag =
+  implicit_args := { !implicit_args with maximal = flag }
+
 let is_implicit_args () = !implicit_args.main
 let is_strict_implicit_args () = !implicit_args.strict
-let is_strong_strict_implicit_args () = !implicit_args.strong_strict
+let is_strongly_strict_implicit_args () = !implicit_args.strongly_strict
 let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern
 let is_contextual_implicit_args () = !implicit_args.contextual
+let is_maximal_implicit_args () = !implicit_args.maximal
 
 let with_implicits flags f x =
   let oflags = !implicit_args in
@@ -156,19 +162,23 @@ let is_flexible_reference env bound depth f =
 
 let push_lift d (e,n) = (push_rel d e,n+1)
 
+let is_reversible_pattern bound depth f l =
+  isRel f & let n = destRel f in (n < bound+depth) & (n >= depth) & 
+  array_for_all (fun c -> isRel c & destRel c < depth) l &
+  array_distinct l
+
 (* Precondition: rels in env are for inductive types only *)
-let add_free_rels_until strict strong_strict revpat bound env m pos acc =
+let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
   let rec frec rig (env,depth as ed) c =
     let hd = if strict then whd_betadeltaiota env c else c in
-    let c = if strong_strict then hd else c in
+    let c = if strongly_strict then hd else c in
     match kind_of_term hd with
     | Rel n when (n < bound+depth) & (n >= depth) ->
-        acc.(bound+depth-n-1) <- update pos rig (acc.(bound+depth-n-1))
-    | App (f,l) when rig & isRel f & revpat ->
-	let n = destRel f in
-	if (n < bound+depth) & (n >= depth) & array_distinct l &
-	  array_for_all (fun c -> isRel c & destRel c < depth) l
-	then acc.(bound+depth-n-1) <- update pos rig (acc.(bound+depth-n-1))
+	let i = bound + depth - n - 1 in
+        acc.(i) <- update pos rig acc.(i)
+    | App (f,l) when revpat & is_reversible_pattern bound depth f l ->
+	let i = bound + depth - destRel f - 1 in
+	acc.(i) <- update pos rig acc.(i)
     | App (f,_) when rig & is_flexible_reference env bound depth f ->
 	if strict then () else
           iter_constr_with_full_binders push_lift (frec false) ed c
@@ -182,19 +192,19 @@ let add_free_rels_until strict strong_strict revpat bound env m pos acc =
 
 (* calcule la liste des arguments implicites *)
 
-let compute_implicits_gen strict strong_strict revpat contextual env t =
+let compute_implicits_gen strict strongly_strict revpat contextual env t =
   let rec aux env avoid n names t =
     let t = whd_betadeltaiota env t in
     match kind_of_term t with
       | Prod (na,a,b) ->
 	  let na',avoid' = Termops.concrete_name None avoid names na b in
-	  add_free_rels_until strict strong_strict revpat n env a (Hyp (n+1))
+	  add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1))
             (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b)
       | _ -> 
 	  let names = List.rev names in
 	  let v = Array.map (fun na -> na,None) (Array.of_list names) in
 	  if contextual then
-	    add_free_rels_until strict strong_strict revpat n env t Conclusion v
+	    add_free_rels_until strict strongly_strict revpat n env t Conclusion v
 	  else v
   in 
   match kind_of_term (whd_betadeltaiota env t) with 
@@ -207,16 +217,16 @@ let compute_implicits_gen strict strong_strict revpat contextual env t =
 let compute_implicits_auto env f t =
   let l =
     compute_implicits_gen 
-      f.strict f.strong_strict f.reversible_pattern f.contextual env t in
+      f.strict f.strongly_strict f.reversible_pattern f.contextual env t in
   List.map (function
-    | (Name id, Some imp) -> Some (id,imp)
+    | (Name id, Some imp) -> Some (id,imp,f.maximal)
     | (Anonymous, Some _) -> anomaly "Unnamed implicit"
     | _ -> None) l
 
 let compute_implicits env t = compute_implicits_auto env !implicit_args t
 
-let set_implicit id imp =
-  Some (id,match imp with None -> Manual | Some imp -> imp)
+let set_implicit id imp insmax =
+  (id,(match imp with None -> Manual | Some imp -> imp),insmax)
 
 let compute_manual_implicits flags ref l =
   let t = Global.type_of_global ref in
@@ -227,33 +237,42 @@ let compute_manual_implicits flags ref l =
     error ("Some parameters are referred more than once");
   (* Compare with automatic implicits to recover printing data and names *)
   let rec merge k l = function
-    | (Name id,imp)::imps ->
-	let l',imp =
-	  try list_remove_first (ExplByPos k) l, set_implicit id imp
-	  with Not_found ->
-	  try list_remove_first (ExplByName id) l, set_implicit id imp
-	  with Not_found ->
-	  l, None in
-	imp :: merge (k+1) l' imps
-    | (Anonymous,imp)::imps -> 
-	None :: merge (k+1) l imps
-    | [] when l = [] -> []
-    | _ ->
-	match List.hd l with
-	| ExplByName id ->
-	    error ("Wrong or not dependent implicit argument name: "^(string_of_id id))
-	| ExplByPos i ->
-	    if i<1 or i>n then 
-	      error ("Bad implicit argument number: "^(string_of_int i))
-	    else
-	      errorlabstrm ""
-		(str "Cannot set implicit argument number " ++ int i ++
-		 str ": it has no name") in
+  | (Name id,imp)::imps ->
+      let l',m =
+	try 
+	  let b = List.assoc (ExplByName id) l in
+	  List.remove_assoc (ExplByName id) l, Some b
+	with Not_found ->
+	try 
+	  let b = List.assoc (ExplByPos k) l in
+	  List.remove_assoc (ExplByPos k) l, Some b
+	with Not_found ->
+	l, None in
+      let imps' = merge (k+1) l' imps in
+      (* Force maximal insertion on ending implicits (compatibility) *)
+      let m = option_map ((||) (List.for_all ((<>) None) imps')) m in
+      option_map (set_implicit id imp) m :: imps'
+  | (Anonymous,_imp)::imps -> 
+      None :: merge (k+1) l imps
+  | [] when l = [] -> []
+  | _ ->
+      match List.hd l with
+      | ExplByName id,_ ->
+	  error ("Wrong or not dependent implicit argument name: "^(string_of_id id))
+      | ExplByPos i,_ ->
+	  if i<1 or i>n then 
+	    error ("Bad implicit argument number: "^(string_of_int i))
+	  else
+	    errorlabstrm ""
+	      (str "Cannot set implicit argument number " ++ int i ++
+	      str ": it has no name") in
   merge 1 l autoimps
 
+type maximal_insertion = bool (* true = maximal contextual insertion *)
+
 type implicit_status =
     (* None = Not implicit *)
-    (identifier * implicit_explanation) option
+    (identifier * implicit_explanation * maximal_insertion) option
 
 type implicits_list = implicit_status list
 
@@ -263,18 +282,22 @@ let is_status_implicit = function
 
 let name_of_implicit = function
   | None -> anomaly "Not an implicit argument"
-  | Some (id,_) -> id
+  | Some (id,_,_) -> id
+
+let maximal_insertion_of = function
+  | Some (_,_,b) -> b
+  | None -> anomaly "Not an implicit argument"
 
 (* [in_ctx] means we now the expected type, [n] is the index of the argument *)
 let is_inferable_implicit in_ctx n = function
   | None -> false
-  | Some (_,DepRigid (Hyp p)) -> n >= p
-  | Some (_,DepFlex (Hyp p)) -> false
-  | Some (_,DepFlexAndRigid (_,Hyp q)) -> n >= q
-  | Some (_,DepRigid Conclusion) -> in_ctx
-  | Some (_,DepFlex Conclusion) -> false
-  | Some (_,DepFlexAndRigid (_,Conclusion)) -> false
-  | Some (_,Manual) -> true
+  | Some (_,DepRigid (Hyp p),_) -> in_ctx or n >= p
+  | Some (_,DepFlex (Hyp p),_) -> false
+  | Some (_,DepFlexAndRigid (_,Hyp q),_) -> in_ctx or n >= q
+  | Some (_,DepRigid Conclusion,_) -> in_ctx
+  | Some (_,DepFlex Conclusion,_) -> false
+  | Some (_,DepFlexAndRigid (_,Conclusion),_) -> in_ctx
+  | Some (_,Manual,_) -> true
 
 let positions_of_implicits =
   let rec aux n = function
@@ -283,9 +306,6 @@ 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 *)
-
 (*s Constants. *)
 
 let compute_constant_implicits flags cst =
@@ -341,7 +361,9 @@ let compute_global_implicits flags = function
 
 (* Caching implicits *)
 
-type implicit_interactive_request = ImplAuto | ImplManual of explicitation list
+type implicit_interactive_request =
+  | ImplAuto
+  | ImplManual of (explicitation * bool) list
 
 type implicit_discharge_request =
   | ImplNoDischarge
diff --git a/library/impargs.mli b/library/impargs.mli
index 41554412dc..8e6e25194e 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -21,15 +21,17 @@ open Nametab
 
 val make_implicit_args : bool -> unit
 val make_strict_implicit_args : bool -> unit
-val make_strong_strict_implicit_args : bool -> unit
+val make_strongly_strict_implicit_args : bool -> unit
 val make_reversible_pattern_implicit_args : bool -> unit
 val make_contextual_implicit_args : bool -> unit
+val make_maximal_implicit_args : bool -> unit
 
 val is_implicit_args : unit -> bool
 val is_strict_implicit_args : unit -> bool
-val is_strong_strict_implicit_args : unit -> bool
+val is_strongly_strict_implicit_args : unit -> bool
 val is_reversible_pattern_implicit_args : unit -> bool
 val is_contextual_implicit_args : unit -> bool
+val is_maximal_implicit_args : unit -> bool
 
 type implicits_flags
 val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b
@@ -42,6 +44,7 @@ type implicits_list = implicit_status list
 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 positions_of_implicits : implicits_list -> int list
 
@@ -59,6 +62,6 @@ val declare_implicits : bool -> global_reference -> unit
 
 (* Manual declaration of which arguments are expected implicit *)
 val declare_manual_implicits : bool -> global_reference -> 
-  Topconstr.explicitation list -> unit
+  (Topconstr.explicitation * bool) list -> unit
 
 val implicits_of_global : global_reference -> implicits_list
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f816001578..8c6e1a547f 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -466,13 +466,17 @@ GEXTEND Gram
 	     [ local = [ IDENT "Global" -> false | IDENT "Local" -> true ];
 	       qid = global -> (local,qid,None) 
 	     | qid = global;
-	       l = OPT [ "["; l = LIST0 ident; "]" -> 
-		   List.map (fun id -> ExplByName id) l ] -> (true,qid,l) ] ->
+	       l = OPT [ "["; l = LIST0 implicit_name; "]" -> 
+		   List.map (fun (id,b) -> (ExplByName id,b)) l ] ->
+		 (true,qid,l) ] ->
 	   VernacDeclareImplicits (local,qid,pos)
 
       | IDENT "Implicit"; ["Type" | IDENT "Types"];
 	   idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ]
   ;
+  implicit_name:
+    [ [ id = ident -> (id,false) | "["; id = ident; "]" -> (id,true) ] ]
+  ;
 END
 
 GEXTEND Gram
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index e9d960e37c..7ccd8dd65d 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -146,9 +146,11 @@ let pr_search a b pr_p = match a with
 let pr_locality local = if local then str "Local " else str ""
 let pr_non_globality local = if local then str "" else str "Global "
 
-let pr_explanation imps = function
-  | ExplByPos n -> pr_id (Impargs.name_of_implicit (List.nth imps (n-1)))
-  | ExplByName id -> pr_id id
+let pr_explanation (e,b) =
+  let a = match e with
+  | ExplByPos n -> anomaly "No more supported"
+  | ExplByName id -> pr_id id in
+  if b then str "[" ++ a ++ str "]" else a
 
 let pr_class_rawexpr = function
   | FunClass -> str"Funclass"
@@ -753,13 +755,10 @@ let rec pr_vernac = function
          pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
   | VernacDeclareImplicits (local,q,None) ->
       hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q)
-  | VernacDeclareImplicits (local,q,Some l) ->
-      let r = Nametab.global q in
-      Impargs.declare_manual_implicits local r l;
-      let imps = Impargs.implicits_of_global r in
+  | VernacDeclareImplicits (local,q,Some imps) ->
       hov 1 (str"Implicit Arguments" ++ pr_non_globality local ++
       spc() ++ pr_reference q ++ spc() ++
-             str"[" ++ prlist_with_sep sep (pr_explanation imps) l ++ str"]")
+             str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
   | VernacReserve (idl,c) ->
       hov 1 (str"Implicit Type" ++
         str (if List.length idl > 1 then "s " else " ") ++
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 64f6de12d2..4d311b177b 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -61,26 +61,24 @@ let print_closed_sections = ref false
 (********************************)
 (** Printing implicit arguments *)
 			  		  
-let print_impl_args_by_pos = function
-  | []  -> mt ()
-  | [i] -> str"Position [" ++ int i ++ str"] is implicit" ++ fnl()
-  | l   -> 
-      str"Positions [" ++ 
-      prlist_with_sep (fun () -> str "; ") int l ++
-      str"] are implicit" ++ fnl()
+let conjugate_to_be = function [_] -> "is" | _ -> "are"
+
+let pr_implicit imp = pr_id (name_of_implicit imp)
 
-let print_impl_args_by_name = function
+let print_impl_args_by_name max = function
   | []  -> mt ()
-  | [i] -> str"Argument " ++ pr_id (name_of_implicit i) ++ str" is implicit" ++
-      fnl()
-  | l   -> 
-      str"Arguments " ++ 
-      prlist_with_sep (fun () -> str ", ")
-        (fun imp -> pr_id (name_of_implicit imp)) l ++
-      str" are implicit" ++ fnl()
+  | impls -> 
+      hov 0 (str (plural (List.length impls) "Argument") ++ spc() ++ 
+      prlist_with_sep pr_coma pr_implicit impls ++ spc() ++ 
+      str (conjugate_to_be impls) ++ str" implicit" ++
+      (if max then strbrk " and maximally inserted" else mt())) ++ fnl()
 
 let print_impl_args l = 
-  print_impl_args_by_name (List.filter is_status_implicit l)
+  let imps = List.filter is_status_implicit l in
+  let maximps = List.filter Impargs.maximal_insertion_of imps in
+  let nonmaximps = list_subtract imps maximps in
+  print_impl_args_by_name false nonmaximps ++
+  print_impl_args_by_name true maximps
 
 (*********************)
 (** Printing Scopes  *)
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 38c5b827fd..7949ef7b2c 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -8,3 +8,7 @@ d2 = fun x : nat => d1 (y:=x)
 
 Arguments x, x0 are implicit
 Argument scopes are [nat_scope nat_scope _]
+map id (1 :: nil)
+     : list nat
+map id' (1 :: nil)
+     : list nat
diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v
index 0ff7e87f37..4c6f2b5dd9 100644
--- a/test-suite/output/Implicit.v
+++ b/test-suite/output/Implicit.v
@@ -17,3 +17,22 @@ Definition d1 y x (h : x = y :>nat) := h.
 Definition d2 x := d1 (y:=x).
 
 Print d2.
+
+(* Check maximal insertion of implicit *)
+
+Require Import List.
+
+Open Scope list_scope.
+
+Set Implicit Arguments.
+Set Maximal Implicit Insertion.
+
+Definition id (A:Type) (x:A) := x.
+
+Check map id (1::nil).
+
+Definition id' (A:Type) (x:A) := x.
+
+Implicit Arguments id' [[A]].
+
+Check map id' (1::nil).
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b4777a43de..433b561c1c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -710,9 +710,9 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "strong strict implicit arguments";
-      optkey   = (TertiaryTable ("Strong","Strict","Implicit"));
-      optread  = Impargs.is_strong_strict_implicit_args;
-      optwrite = Impargs.make_strong_strict_implicit_args }
+      optkey   = (TertiaryTable ("Strongly","Strict","Implicit"));
+      optread  = Impargs.is_strongly_strict_implicit_args;
+      optwrite = Impargs.make_strongly_strict_implicit_args }
 
 let _ =
   declare_bool_option 
@@ -735,8 +735,8 @@ let _ =
     { optsync  = true;
       optname  = "maximal insertion of implicit";
       optkey   = (TertiaryTable ("Maximal","Implicit","Insertion"));
-      optread  = (fun () -> !Constrintern.insert_maximal_implicit);
-      optwrite = (fun b ->  Constrintern.insert_maximal_implicit := b) }
+      optread  = Impargs.is_maximal_implicit_args;
+      optwrite = Impargs.make_maximal_implicit_args }
 
 let _ =
   declare_bool_option 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 042ef1e859..5c1b138550 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -260,7 +260,7 @@ type vernac_expr =
   | VernacSyntacticDefinition of identifier * constr_expr * locality_flag *
       onlyparsing_flag
   | VernacDeclareImplicits of locality_flag * lreference *
-      explicitation list option
+      (explicitation * bool) list option
   | VernacReserve of lident list * constr_expr
   | VernacSetOpacity of opacity_flag * lreference list
   | VernacUnsetOption of Goptions.option_name