aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-02-18 22:18:00 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-02-18 22:18:00 +0000
commit390d8d413fca6d3e0f0f6680d37ddad9a5b6d830 (patch)
treed5141ca2d31a9d70f43aa2245b4183c48ae85a95 /contrib
parent07c8ffdb6364aece263dc86174703190a5236dc4 (diff)
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
Diffstat (limited to 'contrib')
-rw-r--r--contrib/interface/xlate.ml2
1 files changed, 1 insertions, 1 deletions
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)