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

4 files changed, 15 insertions, 5 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index d5de74f8a..537978269 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 9a9c55ec1..a0f8661cc 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 77e6ba42c..9b3268930 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 edbf9fb62..d7634d6e0 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