Global Notation for nat can be confusing
Gappa plugin defines a global notation for nat. This leads to confusing output. In my opinion generic entities like nat should have only local or parsing only notations.
Require Import Gappa.Gappa_tactic.
Search Z nat.
(*
BinIntDef.Z.of_nat: index -> Z
BinIntDef.Z.abs_nat: Z -> index
BinIntDef.Z.to_nat: Z -> index
Zpower.two_power_nat: index -> Z
Z.of_nat: index -> Z
Z.to_nat: Z -> index
Z.abs_nat: Z -> index
*)
Locate index.
(*
Notation Gappa.Gappa_tree.index
*)
Btw.: if index is defined otherwise (which is not rare) one gets Gappa_tree.index
for nat everywhere after Import Gappa.Gappa_tactic
.