ind_tables: always declare side effects (Closes: HOTT#110)

declare takes care of ignoring side effects that are available in the
global environment.  This is yet another instance of what the "abominion"
(aka abstract) can do: the code was checking for the existence in the
environment of the elimination principle, and not regenerating it (nor
declaring the corresponding side effect) if the elimination principle
is used twice.
Of course to functionalize the imperative actions on the environment
when two proofs generated by abstract use the same elim principle,
such elim principle has to be inlined twice, once in each abstracted
proof.  In other words, a side effect generated by a tactic inside
an abstract is *global* but will be made local, si it must always
be declared, no matter what.

Now the system works like this:
- side effects are always declared, even if a caching mechanism thinks
  the constant is already there (it can be there, no need to regenerate it
  but the intent to generate it *must* be declared anyhow)
- at Qed time, we filter the list of side effects and decide which ones are
  really needed to be inlined.

bottom line: STOP using abstract.

1 files changed, 23 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_110.v b/test-suite/bugs/closed/HoTT_coq_110.v
new file mode 100644
index 000000000..5ec40dbcb
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_110.v
@@ -0,0 +1,23 @@
+Module X.
+  Inductive paths A (x : A) : A -> Type := idpath : paths A x x.
+  Notation "x = y" := (@paths _ x y) : type_scope.
+
+  Axioms A B : Type.
+  Axiom P : A = B.
+  Definition foo : A = B.
+    abstract (rewrite <- P; reflexivity).
+  (* Error: internal_paths_rew already exists. *)
+  Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
+End X.
+
+Module Y.
+  Inductive paths A (x : A) : A -> Type := idpath : paths A x x.
+  Notation "x = y" := (@paths _ x y) : type_scope.
+
+  Axioms A B : Type.
+  Axiom P : A = B.
+  Definition foo : (A = B) * (A = B).
+    split; abstract (rewrite <- P; reflexivity).
+  (* Error: internal_paths_rew already exists. *)
+  Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
+End Y.