aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-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 355abd135a..22a282a0f1 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -45,7 +45,7 @@ Hashtbl.add type_table "Coq.Init.Datatypes.nat"
Hashtbl.add type_table "Coq.ZArith.fast_integer.Z"
[|[|"";"ZERO";"POS";"NEG"|]|];;
-Hashtbl.add type_table "Coq.Zarith.fast_integer.positive"
+Hashtbl.add type_table "Coq.ZArith.fast_integer.positive"
[|[|"";"xI";"xO";"XH"|]|];;
(*The following two codes are added to cope with the distinction