diff options
| author | herbelin | 2003-05-20 08:55:34 +0000 |
|---|---|---|
| committer | herbelin | 2003-05-20 08:55:34 +0000 |
| commit | 7eb3b862ab4220b1781fbea69ad4658ac93e7bb1 (patch) | |
| tree | 29b1168ddfd5027cd61325fe87c5092939c5a8e7 | |
| parent | aed2dabdf7e5f72330ff3a6979fece97d4d044ce (diff) | |
Extension renommage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4037 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | library/nameops.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/library/nameops.ml b/library/nameops.ml index cb1c90e50e..7a4ffa8025 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -31,6 +31,7 @@ let translate_v7_string = function | "convert_compare_INFERIEUR" -> "convert_compare_LESS" | "convert_compare_SUPERIEUR" -> "convert_compare_GREATER" | "convert_compare_EGAL" -> "convert_compare_EQUAL" + | "Zcompare_EGAL" -> "Zcompare_EQUAL" | "Nul" -> "Null" | "Un_suivi_de" -> "double_plus_one" | "Zero_suivi_de" -> "double" @@ -44,6 +45,8 @@ let translate_v7_string = function | "min_sym" -> "min_comm" | "gt_not_sym" -> "gt_asym" | "fact_growing" -> "fact_le" + (* Lists *) + | "idempot_rev" -> "involutive_rev" (* Bool *) | "orb_sym" -> "orb_comm" | "andb_sym" -> "andb_comm" |