diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-04 12:58:19 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-04 12:58:19 +0000 |
| commit | 5f42f80fb84f8fa8137eb73531bcdbebc1057270 (patch) | |
| tree | e5d30f7942c38d079e0796ee47ae069bb7aa0f6c /contrib | |
| parent | d7121ac57d10609aeb58fd84db4be8038c3247cf (diff) | |
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
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/interface/xlate.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 8d4d952b5..85e750b20 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 |