After importing QArith in Coq
Require Import Coq.QArith.QArith_base.
I want to define a product type
Parameter T : Type.
Definition TT : Type := T * T.
but the * is redefined in QArith, and I get the error message
Error: The term "T" has type "Type" while it is expected to have type "Q".
How can I use the original *?
In a sense there is no "original" *. Notations can be overloaded and reused and usually Coq is clever enough to pick the right interpretation for a notation. But sometimes you need to explicitly tell Coq what interpretation scope to use.
The reference manual says that (sect. 12.2):
An interpretation scope is a set of notations for terms with their interpretation. Interpretation scopes provide a weak, purely syntactical form of notation overloading: the same notation, for instance the infix symbol
+, can be used to denote distinct definitions of the additive operator. Depending on which interpretation scope is currently open, the interpretation is different. Interpretation scopes can include an interpretation for numerals and strings.
Let me mention a useful command to find out more about notations and their interpretation scope: Locate "*". will give you the list of things * unfolds into, together with the names of interpretation scopes and the default interpretation scope.
Coq as of version 8.4pl4 tries to use the default interpretation scope, which is Q_scope in your case -- that's why you see the error. It can be easily fixed e.g. with scope annotation:
Definition TT : Type := (T * T) % type.
However, more recent Coq versions (like 8.7.0) understand that in that context we should use type_scope, so your code snippet works without any modification.