From 509940521cda3057455adb0f0af8b16d88b73df6 Mon Sep 17 00:00:00 2001
From: bertot
Date: Sat, 7 Apr 2001 08:44:10 +0000
Subject: Make sure the parser knows about the constructors of type nat, so
 that specific syntax for this type can be parsed and translated to tree
 structures.

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

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 85e750b201..3260796330 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -39,6 +39,9 @@ Hashtbl.add type_table "Coq.Init.Logic.and"
 Hashtbl.add type_table "Coq.Init.Datatypes.prod"
   [|[|"dummy";"pair"|]|];;
 
+Hashtbl.add type_table "Coq.Init.Datatypes.nat"
+  [|[|"";"O"; "S"|]|];;
+
 Hashtbl.add type_table "Coq.Zarith.fast_integer.Z"
 [|[|"";"ZERO";"POS";"NEG"|]|];;
 
-- 
cgit v1.2.3