coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] The same id. name has difference types!

From: xiang sen <xiangsen AT ustc.edu>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] The same id. name has difference types!
Date: Mon, 04 Jul 2005 22:25:29 +0800
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi all,

I inversion one hypothesis and generate serveral bypo, and
coincidentally there are two id. owning the same name.
such as :
p : nat
p' : nat
q : nat
H34 : p = lookupR rf p
H35 : q = 0
H27 : h1 = x9
H29 : rf1 = rf
_________________________
....................

where one p is of "nat', one is of "reg". When I reference p as "reg",
coqtop reports errors and does not work as expected.
How to resolve it?

Thanks

Best
Xiang Sen

[Coq-Club] The same id. name has difference types!, xiang sen
- Re: [Coq-Club] The same id. name has difference types!, Pierre Casteran