Reviewed-by: ppedrot

Ack-by: JasonGross
Reviewed-by: herbelin
Reviewed-by: jashug
Reviewed-by: jfehrle
Reviewed-by: ppedrot

We also get rid of ploc.ml, now useless, relying a priori on more
robust code in lStream.ml for location reporting (see
e.g. parse_parsable in grammar.ml).

Reviewed-by: mattam82
Ack-by: Zimmi48

Reviewed-by: ppedrot

Reviewed-by: Zimmi48
Reviewed-by: vbgl

`Global.lookup_constant` fails with an assertion instead of `Not_found`. Some
code relied upon `Not_found`.

- to zify the conclusion, we are using Tactics.apply (not rewrite)

Closes #11089

- constrain the arguments of Add Zify X to be GlobRef.t
Unset Primitive Projections so that projections are GlobRef.t.

Closes #14043

Update doc/sphinx/addendum/micromega.rst

Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>

The role of the `zify_saturate` tactic is to augment the goal with
positivity constraints.  The premisses were previously obtained from
the context. If they are not present, we instantiate the saturation
lemma anyway.

Also,
- Remove saturation rules for Z.mul, the reasoning is performed by lia/nia
- Run zify_saturate after zify_to_euclidean_division_equations
- Better lemma for Z.power
- Ensure that lemma are generated once

Co-authored-by:  Andrej Dudenhefner  <mrhaandi>

Closes #12184, #11656

Reviewed-by: vbgl