From 5f42f80fb84f8fa8137eb73531bcdbebc1057270 Mon Sep 17 00:00:00 2001
From: bertot
Date: Wed, 4 Apr 2001 12:58:19 +0000
Subject: Make sure the constructors of Z and positive are recognized: they
 show up when parsing expressions between back-quotes.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1538 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/xlate.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 8d4d952b5f..85e750b201 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -39,6 +39,12 @@ Hashtbl.add type_table "Coq.Init.Logic.and"
 Hashtbl.add type_table "Coq.Init.Datatypes.prod"
   [|[|"dummy";"pair"|]|];;
 
+Hashtbl.add type_table "Coq.Zarith.fast_integer.Z"
+[|[|"";"ZERO";"POS";"NEG"|]|];;
+
+Hashtbl.add type_table "Coq.Zarith.fast_integer.positive"
+[|[|"";"xI";"xO";"XH"|]|];;
+
 (*The following two codes are added to cope with the distinction
   between ocaml and caml-light syntax while using ctcaml to
   manipulate the program *)
@@ -415,7 +421,8 @@ let xlate_op the_node opn a b =
 	     xlate_error
 	       ("MUTCONSTRUCT:" ^ 
                 " can't describe a constructor without its name " ^
-		name)
+		name ^ "(" ^ (string_of_int tyi) ^ "," ^
+	       (string_of_int n) ^ ")")
          | Some type_desc' -> 
               let type_desc'' = type_desc'.(tyi) in
               let ident = type_desc''.(n) in
-- 
cgit v1.2.3