fix axiom counting

[fblanqui]

A.lp:

symbol A:TYPE;

B.lp:

symbol B:TYPE;

bug.lp

require open Stdlib.A;
symbol a:A ≔ begin admit end;
require open Stdlib.B;
symbol b:B ≔ begin admit end;

was generating 2 axioms with the same name (namely _ax0) because each require reset the axiom counter.
This PR:

• fixes that bug (in compile.ml and tactic.ml)
• make Sign.add_symbol check that the signature does not already have a symbol with the same name
• add Term.qsym
• remove Print.path (= Path.pp)
• replace Term.is_ac by Term.is_modulo