Multiples changements autour des implicites :

- correction du mode strict qui n'était pas si strict,
- option "Set Strong Strict Implicit" pour activer le mode strictement
  strict (désactivé par défaut pour raison de compatibilité),
- option "Set Reversible Pattern Implicit" pour activer les implicites
  inférables par unification-pattern (désactivé par défaut par compatibilité),
- option "Unset Printing Implicit Defensive" pour désactiver
  l'affichage des implicites n'ayant pas été décelés stricts,
- option "Set Maximal Implicit Insertion" pour que les
  applications soient saturées en implicites si possible,
- une optimisation du mode non strict pour que l'algo de
  recherche des implicites renonce à calculer les occurrences non
  strictes qui pourraient avoir à être affichées dans le mode défensif,
  avec pour conséquence que le mode défensif, pour celui qui le veut,
  devient a priori encore plus verbeux, ex:

  Set Implicit Arguments.
  Definition id x : nat := x.
  Parameter f : forall n, id n = id n -> Prop.
  Check (f (refl_equal O)).
  (* Affichait: "f (refl_equal 0)" mais affiche maintenant 
     "f (n:=0) (refl_equal 0)" *)



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

8 files changed, 117 insertions, 50 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index d5de74f8ab..537978269c 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -44,11 +44,15 @@ let print_evar_arguments = ref false
 (* This governs printing of implicit arguments.  When
    [print_implicits] is on then [print_implicits_explicit_args] tells
    how implicit args are printed. If on, implicit args are printed
-   prefixed by "!" otherwise the function and not the arguments is
-   prefixed by "!" *)
+   with the form (id:=arg) otherwise arguments are printed normally and
+   the function is prefixed by "@" *)
 let print_implicits = ref false
 let print_implicits_explicit_args = ref false
 
+(* Tells if implicit arguments not known to be inferable from a rigid
+   position are systematically printed *)
+let print_implicits_defensive = ref true
+
 (* This forces printing of coercions *)
 let print_coercions = ref false
 
@@ -503,8 +507,9 @@ let explicitize loc inctx impl (cf,f) args =
         let visible =
           !Options.raw_print or
           (!print_implicits & !print_implicits_explicit_args) or 
-	  (is_significant_implicit a impl tail &
-	  (not (is_inferable_implicit inctx n imp)))
+	  (!print_implicits_defensive &
+	   is_significant_implicit a impl tail &
+	   not (is_inferable_implicit inctx n imp))
 	in
         if visible then 
 	  (a,Some (dummy_loc, ExplByName (name_of_implicit imp))) :: tail 
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 9a9c55ec1d..a0f8661ccd 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -45,6 +45,7 @@ val extern_sort : sorts -> rawsort
 
 (* Printing options *)
 val print_implicits : bool ref
+val print_implicits_defensive : bool ref
 val print_arguments : bool ref
 val print_evar_arguments : bool ref
 val print_coercions : bool ref
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 77e6ba42cf..9b3268930c 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -44,6 +44,8 @@ let for_grammar f x =
 
 let variables_bind = ref false
 
+let insert_maximal_implicit = ref false
+
 (**********************************************************************)
 (* Internalisation errors                                             *)
 
@@ -1033,7 +1035,7 @@ 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=[] &
+	  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 *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index edbf9fb62a..d7634d6e09 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -47,6 +47,8 @@ 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 fc247f8c1c..2caf4d1108 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -25,46 +25,54 @@ open Topconstr
 
 (*s Flags governing the computation of implicit arguments *)
 
+type implicits_flags = {
+  main : bool;
+  strict : bool;
+  strong_strict : bool;
+  reversible_pattern : bool;
+  contextual : bool
+}
+
 (* les implicites sont stricts par défaut en v8 *)
-let implicit_args = ref false
-let strict_implicit_args = ref true
-let contextual_implicit_args = ref false
+
+let implicit_args = ref { 
+  main = false;
+  strict = true;
+  strong_strict = false;
+  reversible_pattern = false;
+  contextual = false
+}
 
 let make_implicit_args flag =
-  implicit_args := flag
+  implicit_args := { !implicit_args with main = flag }
 
 let make_strict_implicit_args flag =
-  strict_implicit_args := flag
+  implicit_args := { !implicit_args with strict = flag }
 
-let make_contextual_implicit_args flag =
-  contextual_implicit_args := flag
+let make_strong_strict_implicit_args flag =
+  implicit_args := { !implicit_args with strong_strict = flag }
 
-let is_implicit_args () = !implicit_args
-let is_strict_implicit_args () = !strict_implicit_args
-let is_contextual_implicit_args () = !contextual_implicit_args
+let make_reversible_pattern_implicit_args flag =
+  implicit_args := { !implicit_args with reversible_pattern = flag }
 
-type implicits_flags = bool * bool * bool
+let make_contextual_implicit_args flag =
+  implicit_args := { !implicit_args with contextual = flag }
 
-let implicit_flags () = 
-  (!implicit_args, !strict_implicit_args, !contextual_implicit_args)
+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_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern
+let is_contextual_implicit_args () = !implicit_args.contextual
 
-let with_implicits (a,b,c) f x =
-  let oa = !implicit_args in
-  let ob = !strict_implicit_args in
-  let oc = !contextual_implicit_args in
+let with_implicits flags f x =
+  let oflags = !implicit_args in
   try 
-    implicit_args := a;
-    strict_implicit_args := b;
-    contextual_implicit_args := c;
-    let rslt = f x in 
-    implicit_args := oa;
-    strict_implicit_args := ob;
-    contextual_implicit_args := oc;
+    implicit_args := flags;
+    let rslt = f x in
+    implicit_args := oflags;
     rslt
   with e -> begin
-    implicit_args := oa;
-    strict_implicit_args := ob;
-    contextual_implicit_args := oc;
+    implicit_args := oflags;
     raise e
   end
 
@@ -149,11 +157,18 @@ let is_flexible_reference env bound depth f =
 let push_lift d (e,n) = (push_rel d e,n+1)
 
 (* Precondition: rels in env are for inductive types only *)
-let add_free_rels_until strict bound env m pos acc =
+let add_free_rels_until strict strong_strict revpat bound env m pos acc =
   let rec frec rig (env,depth as ed) c =
-    match kind_of_term (whd_betadeltaiota env c) with
+    let hd = if strict then whd_betadeltaiota env c else c in
+    let c = if strong_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))
     | 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
@@ -167,18 +182,19 @@ let add_free_rels_until strict bound env m pos acc =
 
 (* calcule la liste des arguments implicites *)
 
-let compute_implicits_gen strict contextual env t =
+let compute_implicits_gen strict strong_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 n env a (Hyp (n+1))
+	  add_free_rels_until strict strong_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 n env t Conclusion v
+	  if contextual then
+	    add_free_rels_until strict strong_strict revpat n env t Conclusion v
 	  else v
   in 
   match kind_of_term (whd_betadeltaiota env t) with 
@@ -188,21 +204,24 @@ let compute_implicits_gen strict contextual env t =
 	Array.to_list v
     | _ -> []
 
-let compute_implicits_auto env (_,strict,contextual) t =
-  let l = compute_implicits_gen strict contextual env t in
+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
   List.map (function
     | (Name id, Some imp) -> Some (id,imp)
     | (Anonymous, Some _) -> anomaly "Unnamed implicit"
     | _ -> None) l
 
-let compute_implicits env t = compute_implicits_auto env (implicit_flags()) t
+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 compute_manual_implicits flags ref l =
   let t = Global.type_of_global ref in
-  let autoimps = compute_implicits_gen false true (Global.env()) t in
+  let autoimps =
+    compute_implicits_gen false false false true (Global.env()) t in
   let n = List.length autoimps in
   if not (list_distinct l) then 
     error ("Some parameters are referred more than once");
@@ -390,23 +409,23 @@ let declare_implicits_gen req flags ref =
   add_anonymous_leaf (inImplicits (req,[ref,imps]))
 
 let declare_implicits local ref =
-  let flags = (true,!strict_implicit_args,!contextual_implicit_args) in
+  let flags = { !implicit_args with main = true } in
   let req = 
     if local then ImplNoDischarge else ImplInteractive(ref,flags,ImplAuto) in
   declare_implicits_gen req flags ref
 
 let declare_var_implicits id =
-  if !implicit_args then
-    declare_implicits_gen ImplNoDischarge (implicit_flags ()) (VarRef id)
+  if !implicit_args.main then
+    declare_implicits_gen ImplNoDischarge !implicit_args (VarRef id)
 
 let declare_constant_implicits con =
-  if !implicit_args then
-    let flags = implicit_flags () in
+  if !implicit_args.main then
+    let flags = !implicit_args in
     declare_implicits_gen (ImplConstant (con,flags)) flags (ConstRef con)
 
 let declare_mib_implicits kn =
-  if !implicit_args then
-    let flags = implicit_flags () in
+  if !implicit_args.main then
+    let flags = !implicit_args in
     let imps = array_map_to_list
       (fun (ind,cstrs) -> ind::(Array.to_list cstrs))
       (compute_mib_implicits flags kn) in
@@ -416,7 +435,7 @@ let declare_mib_implicits kn =
 (* Declare manual implicits *)
 
 let declare_manual_implicits local ref l =
-  let flags = !implicit_args,!strict_implicit_args,!contextual_implicit_args in
+  let flags = !implicit_args in
   let l' = compute_manual_implicits flags ref l in
   let req =
     if local or isVarRef ref then ImplNoDischarge
diff --git a/library/impargs.mli b/library/impargs.mli
index 6158610435..41554412dc 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -21,10 +21,14 @@ 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_reversible_pattern_implicit_args : bool -> unit
 val make_contextual_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_reversible_pattern_implicit_args : unit -> bool
 val is_contextual_implicit_args : unit -> bool
 
 type implicits_flags
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 269c40fec3..23e732797a 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -108,7 +108,9 @@ let current_constant id =
   try
     global_reference id
   with Not_found ->
-    anomaly ("Setoid: cannot find " ^ (string_of_id id))
+    anomalylabstrm ""
+      (str "Setoid: cannot find " ++ pr_id id ++
+       str "(if loading Setoid.v under coqtop, use option \"-top Coq.Setoids.Setoid\")")
 
 (* From Setoid.v *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4c0fb5046f..b4777a43de 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -709,6 +709,14 @@ let _ =
 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 }
+
+let _ =
+  declare_bool_option 
+    { optsync  = true;
       optname  = "contextual implicit arguments";
       optkey   = (SecondaryTable ("Contextual","Implicit"));
       optread  = Impargs.is_contextual_implicit_args;
@@ -717,6 +725,22 @@ let _ =
 let _ =
   declare_bool_option 
     { optsync  = true;
+      optname  = "implicit arguments defensive printing";
+      optkey   = (TertiaryTable ("Reversible","Pattern","Implicit"));
+      optread  = Impargs.is_reversible_pattern_implicit_args;
+      optwrite = Impargs.make_reversible_pattern_implicit_args }
+
+let _ =
+  declare_bool_option 
+    { 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) }
+
+let _ =
+  declare_bool_option 
+    { optsync  = true;
       optname  = "coercion printing";
       optkey   = (SecondaryTable ("Printing","Coercions"));
       optread  = (fun () -> !Constrextern.print_coercions);
@@ -733,6 +757,14 @@ let _ =
 let _ =
   declare_bool_option 
     { optsync  = true;
+      optname  = "implicit arguments defensive printing";
+      optkey   = (TertiaryTable ("Printing","Implicit","Defensive"));
+      optread  = (fun () -> !Constrextern.print_implicits_defensive);
+      optwrite = (fun b ->  Constrextern.print_implicits_defensive := b) }
+
+let _ =
+  declare_bool_option 
+    { optsync  = true;
       optname  = "projection printing using dot notation";
       optkey   = (SecondaryTable ("Printing","Projections"));
       optread  = (fun () -> !Constrextern.print_projections);