Applying François' patches about Canonical Projections (see #2302 and #2334).

Printer pr_cs_pattern is kept in recordops only. Also updated CHANGES.
Fixed spelling of "uniform inheritance condition" in doc too (see

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

5 files changed, 31 insertions, 11 deletions

diff --git a/CHANGES b/CHANGES
index 15e7288f67..b53ad69725 100644
--- a/CHANGES
+++ b/CHANGES
@@ -56,7 +56,7 @@ Other tactics
   variables and "**" for introducing all quantified variables and hypotheses.
 - Pattern Unification for existential variables activated in tactics and 
   new option "Unset Tactic Evars Pattern Unification" to deactivate it.
-- Resolution of Canonical Structures is now part of the tactic's unification
+- Resolution of canonical structure is now part of the tactic's unification
   algorithm.
 - New tactic "decide lemma with hyp" for rewriting decidability lemmas
   when one knows which side is true.
@@ -197,6 +197,7 @@ Vernacular commands
   later "Eval <id> in ...". This command accepts a Local variant.
 - Syntax of Implicit Type now supports more than one block of variables of
   a given type.
+- Command "Canonical Structure" now warns when it has no effects.
 
 Library
 
diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex
index 7a74ffd31f..4f3d3ec41e 100644
--- a/doc/refman/Coercion.tex
+++ b/doc/refman/Coercion.tex
@@ -163,7 +163,7 @@ Declares the construction denoted by {\qualid} as a coercion between
 \item {\qualid} \errindex{is not a function}
 \item \errindex{Cannot find the source class of {\qualid}}
 \item \errindex{Cannot recognize {\class$_1$} as a source class of {\qualid}}
-\item {\qualid} \errindex{does not respect the inheritance uniform condition}
+\item {\qualid} \errindex{does not respect the uniform inheritance condition}
 \item \errindex{Found target class {\class} instead of {\class$_2$}}
 
 \end{ErrMsgs}
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index cc04f8f345..1024dce610 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -754,12 +754,6 @@ let print_path_between cls clt =
   in
   print_path ((i,j),p)
 
-let pr_cs_pattern = function
-    Const_cs c -> pr_global c
-  | Prod_cs -> str "_ -> _"
-  | Default_cs -> str "_"
-  | Sort_cs s -> pr_sort_family s
-
 let print_canonical_projections () =
   prlist_with_sep pr_fnl
     (fun ((r1,r2),o) -> pr_cs_pattern r2 ++
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index df0f3e460e..8af707c119 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -235,7 +235,14 @@ let compute_canonical_projections (con,ind) =
 		 try
 		   let patt, n , args = cs_pattern_of_constr t in
 		     ((ConstRef proji_sp, patt, n, args) :: l)
-		 with Not_found -> l
+		 with Not_found ->
+                   if Flags.is_verbose () then
+                     (let con_pp = Nametab.pr_global_env Idset.empty (ConstRef con)
+                      and proji_sp_pp = Nametab.pr_global_env Idset.empty (ConstRef proji_sp) in
+		      msg_warning (str "No global reference exists for projection value"
+                                   ++ print_constr t ++ str " in instance "  
+                                   ++ con_pp ++ str " of " ++ proji_sp_pp ++ str ", ignoring it."));
+		   l
 	       end
 	   | _ -> l)
       [] lps in
@@ -245,13 +252,30 @@ let compute_canonical_projections (con,ind) =
      o_TPARAMS=params; o_NPARAMS=List.length params; o_TCOMPS=argj})
     comp
 
+let pr_cs_pattern = function
+    Const_cs c -> Nametab.pr_global_env Idset.empty c
+  | Prod_cs -> str "_ -> _"
+  | Default_cs -> str "_"
+  | Sort_cs s -> Termops.pr_sort_family s
+
 let open_canonical_structure i (_,o) =
   if i=1 then
     let lo = compute_canonical_projections o in
     List.iter (fun ((proj,cs_pat),s) ->
       let l = try Refmap.find proj !object_table with Not_found -> [] in
-      if not (List.mem_assoc cs_pat l) then
-        object_table := Refmap.add proj ((cs_pat,s)::l) !object_table) lo
+      let ocs = try Some (List.assoc cs_pat l)
+      with Not_found -> None
+      in match ocs with
+        | None -> object_table := Refmap.add proj ((cs_pat,s)::l) !object_table;
+        | Some cs ->
+            if Flags.is_verbose () then
+              let old_can_s = (Termops.print_constr cs.o_DEF)
+              and new_can_s = (Termops.print_constr s.o_DEF) in
+              let prj = (Nametab.pr_global_env Idset.empty proj)
+              and hd_val = (pr_cs_pattern cs_pat) in
+              msg_warning (str "Ignoring canonical projection to " ++ hd_val
+                             ++ str " by " ++ prj ++ str " in "
+                             ++ new_can_s ++ str ": redundant with " ++ old_can_s)) lo
 
 let cache_canonical_structure o =
   open_canonical_structure 1 o
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 6ad5fbc643..88e6c5000b 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -73,6 +73,7 @@ type obj_typ = {
   o_TCOMPS : constr list } (** ordered *)
 
 val cs_pattern_of_constr : constr -> cs_pattern * int * constr list
+val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds
 
 val lookup_canonical_conversion : (global_reference * cs_pattern) -> obj_typ
 val declare_canonical_structure : global_reference -> unit