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

1 files changed, 3 insertions, 1 deletions

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 *)