Fix #7795: UGraph.AlreadyDeclared with Program

This change is based on noticing that we use a default value for the
`sideff` argument even though we have a similarly named `side_eff`
available. Someone who knows how side effects and universes are
supposed to interact should check this.

2 files changed, 67 insertions, 2 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 678c3ea3f7..b48f14ca82 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -173,8 +173,8 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
       const_entry_body = Future.chain ce.const_entry_body
         (fun (pt, _) -> pt, ()) } in
   let (cb, ctx), () = Future.force ce.const_entry_body in
-  let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in
-  cb, status, Evd.evar_universe_context univs'
+  let univs = UState.merge side_eff Evd.univ_rigid univs ctx in
+  cb, status, univs
 
 let refine_by_tactic env sigma ty tac =
   (** Save the initial side-effects to restore them afterwards. We set the
diff --git a/test-suite/bugs/closed/7795.v b/test-suite/bugs/closed/7795.v
new file mode 100644
index 0000000000..5db0f81cc5
--- /dev/null
+++ b/test-suite/bugs/closed/7795.v
@@ -0,0 +1,65 @@
+
+
+Definition fwd (b: bool) A (e2: A): A. Admitted.
+
+Ltac destruct_refinement_aux T :=
+  let m := fresh "mres" in
+  let r := fresh "r" in
+  let P := fresh "P" in
+  pose T as m;
+  destruct m as [ r P ].
+
+Ltac destruct_refinement :=
+  match goal with
+  | |- context[proj1_sig ?T] => destruct_refinement_aux T
+  end.
+
+Ltac t_base := discriminate || destruct_refinement.
+
+
+Inductive List (T: Type) :=
+| Cons_construct: T -> List T -> List T
+| Nil_construct: List T.
+
+Definition t (T: Type): List T. Admitted.
+Definition size (T: Type) (src: List T): nat. Admitted.
+Definition filter1_rt1_type (T: Type): Type := { res: List T | false = true }.
+Definition filter1 (T: Type): filter1_rt1_type T. Admitted.
+
+Definition hh_1:
+  forall T : Type,
+    (forall (T0 : Type),
+     False -> filter1_rt1_type T0) ->
+     False.
+Admitted.
+
+Definition hh_2:
+  forall (T : Type),
+    filter1_rt1_type T ->
+    filter1_rt1_type T.
+Admitted.
+
+Definition hh:
+  forall (T : Type) (f1 : forall (T0 : Type), False -> filter1_rt1_type T0),
+       fwd
+         (Nat.leb
+               (size T
+                  (fwd false (List T)
+                     (fwd false (List T)
+                        (proj1_sig
+                           (hh_2 T
+                              (f1 T (hh_1 T f1))))))) 0) bool
+         false = true.
+Admitted.
+
+Set Program Mode. (* removing this line prevents the bug *)
+Obligation Tactic := repeat t_base.
+
+Goal
+  forall T (h17: T),
+    filter1 T =
+    exist
+      _
+      (Nil_construct T)
+      (hh T (fun (T : Type) (_ : False) => filter1 T)).
+Abort.