Renaming Print Canonical Structure into Print Canonical Projections

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

9 files changed, 13 insertions, 13 deletions

diff --git a/CHANGES b/CHANGES
index 2c865c877..8104f54eb 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,7 +5,7 @@ Vernacular commands
 
 - Added "Print Rewrite HintDb" to print the content of a DB used by
   autorewrite (doc TODO)
-- Added "Print Canonical Structures" (doc TODO)
+- Added "Print Canonical Projections" (doc TODO)
 
 Gallina
 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index f0cdc49ae..60688b625 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1785,7 +1785,7 @@ let rec xlate_vernac =
 	| PrintCoercions -> CT_print_coercions
 	| PrintCoercionPaths (id1, id2) -> 
 	    CT_print_path (xlate_class id1, xlate_class id2)
-	| PrintCanonicalStructures ->
+	| PrintCanonicalConversions ->
 	    xlate_error "TODO: Print Canonical Structures"
 	| PrintInspect n -> CT_inspect (CT_int n)
 	| PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s)
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index a8f46a12b..648bb2829 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -191,7 +191,7 @@ GEXTEND Gram
       | IDENT "Coercions" -> PrintCoercions
       | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
          -> PrintCoercionPaths (s,t)
-      | IDENT "Canonical"; IDENT "Structures" -> PrintCanonicalStructures
+      | IDENT "Canonical"; IDENT "Projections" -> PrintCanonicalConversions
       | IDENT "Tables" -> PrintTables
       | "Proof"; qid = global -> PrintOpaqueName qid
       | IDENT "Hint" -> PrintHintGoal
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 26a38e381..603abd73a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -404,9 +404,8 @@ GEXTEND Gram
       | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
           let s = Ast.coerce_global_to_id qid in
 	  VernacDefinition 
-	    ((Global,CanonicalStructure),(dummy_loc,s),d,Recordobj.add_object_hook)
-      (* Rem: LOBJECT, OBJCOERCION, LOBJCOERCION have been removed
-         (they were unused and undocumented) *)
+	    ((Global,CanonicalStructure),(dummy_loc,s),d,
+	     (fun _ -> Recordops.declare_canonical_structure))
 
 (* Coercions *)
       | IDENT "Coercion"; qid = global; d = def_body ->
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 5b0350f82..a32e32538 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -402,7 +402,8 @@ GEXTEND Gram
       | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
           let s = Ast.coerce_global_to_id qid in
 	  VernacDefinition 
-	    ((Global,CanonicalStructure),(dummy_loc,s),d,Recordobj.add_object_hook)
+	    ((Global,CanonicalStructure),(dummy_loc,s),d,
+	     (fun _ -> Recordops.declare_canonical_structure))
 
       (* Coercions *)
       | IDENT "Coercion"; qid = global; d = def_body ->
@@ -579,7 +580,7 @@ GEXTEND Gram
       | IDENT "Coercions" -> PrintCoercions
       | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
          -> PrintCoercionPaths (s,t)
-      | IDENT "Canonical"; IDENT "Structures" -> PrintCanonicalStructures
+      | IDENT "Canonical"; IDENT "Projections" -> PrintCanonicalConversions
       | IDENT "Tables" -> PrintTables
 (* Obsolete: was used for cooking V6.3 recipes ??
       | IDENT "Proof"; qid = global -> PrintOpaqueName qid
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index a358301e5..eded75be9 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -628,9 +628,9 @@ let print_path_between cls clt =
   in
   print_path ((i,j),p)
 
-let print_canonical_structures () =
+let print_canonical_projections () =
   prlist_with_sep pr_fnl (fun ((r1,r2),o) -> 
     pr_global r2 ++ str " <- " ++ pr_global r1 ++ str " ( " ++ prterm o.o_DEF ++ str " )")
-    (canonical_structures ())
+    (canonical_projections ())
 
 (*************************************************************************)
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index 20429cd3d..4c52420d0 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -57,7 +57,7 @@ val print_graph : unit -> std_ppcmds
 val print_classes : unit -> std_ppcmds
 val print_coercions : unit -> std_ppcmds
 val print_path_between : Classops.cl_typ -> Classops.cl_typ -> std_ppcmds
-val print_canonical_structures : unit -> std_ppcmds
+val print_canonical_projections : unit -> std_ppcmds
 
 val inspect : int -> std_ppcmds
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index db68c779c..2fab2b0da 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -51,7 +51,7 @@ type printable =
   | PrintClasses
   | PrintCoercions
   | PrintCoercionPaths of class_rawexpr * class_rawexpr
-  | PrintCanonicalStructures
+  | PrintCanonicalConversions
   | PrintUniverses of string option
   | PrintHint of reference
   | PrintHintGoal
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index a039027a2..1adc2aeb1 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -1031,7 +1031,7 @@ let rec pr_vernac = function
 	| PrintClasses -> str"Print Classes"
 	| PrintCoercions -> str"Print Coercions"
 	| PrintCoercionPaths (s,t) -> str"Print Coercion Paths" ++ spc() ++ pr_class_rawexpr s ++ spc() ++ pr_class_rawexpr t
-	| PrintCanonicalStructures -> str"Print Canonical Structures"
+	| PrintCanonicalConversions -> str"Print Canonical Structures"
 	| PrintTables -> str"Print Tables"
 	| PrintOpaqueName qid -> str"Print Term" ++ spc() ++ pr_reference qid
 	| PrintHintGoal -> str"Print Hint"