Program: fix #4873: transparency option not used

3 files changed, 88 insertions, 13 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1c50253d9..c0c38a183 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1609,11 +1609,13 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	    (merge_impargs l args) loc
 
     | CRecord (loc, fs) ->
-	let fields =
-	  sort_fields ~complete:true loc fs
-	    (fun _idx -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None))
-	in
-	begin
+       let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
+       let fields =
+	 sort_fields ~complete:true loc fs
+	             (fun _idx -> CHole (loc, Some (Evar_kinds.QuestionMark st),
+                                                 Misctypes.IntroAnonymous, None))
+       in
+       begin
 	  match fields with
 	    | None -> user_err_loc (loc, "intern", str"No constructor inference.")
 	    | Some (n, constrname, args) ->
@@ -1683,7 +1685,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
         GIf (loc, c', (na', p'), intern env b1, intern env b2)
     | CHole (loc, k, naming, solve) ->
         let k = match k with
-        | None -> Evar_kinds.QuestionMark (Evar_kinds.Define true)
+        | None ->
+           let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
+           Evar_kinds.QuestionMark st
         | Some k -> k
         in
         let solve = match solve with
diff --git a/test-suite/bugs/closed/4873.v b/test-suite/bugs/closed/4873.v
new file mode 100644
index 000000000..f2f917b4e
--- /dev/null
+++ b/test-suite/bugs/closed/4873.v
@@ -0,0 +1,72 @@
+Require Import Coq.Classes.Morphisms.
+Require Import Relation_Definitions.
+Require Import Coq.Compat.Coq85.
+
+Fixpoint tuple' T n : Type :=
+  match n with
+  | O => T
+  | S n' => (tuple' T n' * T)%type
+  end.
+
+Definition tuple T n : Type :=
+  match n with
+  | O => unit
+  | S n' => tuple' T n'
+  end.
+
+Fixpoint to_list' {T} (n:nat) {struct n} : tuple' T n -> list T :=
+  match n with
+  | 0 => fun x => (x::nil)%list
+  | S n' => fun xs : tuple' T (S n') => let (xs', x) := xs in (x :: to_list' n' xs')%list
+  end.
+
+Definition to_list {T} (n:nat) : tuple T n -> list T :=
+  match n with
+  | 0 => fun _ => nil
+  | S n' => fun xs : tuple T (S n') => to_list' n' xs
+  end.
+
+Program Fixpoint from_list' {T} (y:T) (n:nat) (xs:list T) : length xs = n -> tuple' T n :=
+  match n return _ with
+  | 0 =>
+    match xs return (length xs = 0 -> tuple' T 0) with
+    | nil => fun _ => y
+    | _ => _ (* impossible *)
+    end
+  | S n' =>
+    match xs return (length xs = S n' -> tuple' T (S n')) with
+    | cons x xs' => fun _ => (from_list' x n' xs' _, y)
+    | _ => _ (* impossible *)
+    end
+  end.
+Goal True.
+  pose from_list'_obligation_3 as e.
+  repeat (let e' := fresh in
+          rename e into e';
+          (pose (e' nat) as e || pose (e' 0) as e || pose (e' nil) as e || pose (e' eq_refl) as e);
+          subst e').
+  progress hnf in e.
+  pose (eq_refl : e = eq_refl).
+  exact I.
+Qed.
+
+Program Definition from_list {T} (n:nat) (xs:list T) : length xs = n -> tuple T n :=
+match n return _ with
+| 0 =>
+    match xs return (length xs = 0 -> tuple T 0) with
+    | nil => fun _ : 0 = 0 => tt
+    | _ => _ (* impossible *)
+    end
+| S n' =>
+    match xs return (length xs = S n' -> tuple T (S n')) with
+    | cons x xs' => fun _ => from_list' x n' xs' _
+    | _ => _ (* impossible *)
+    end
+end.
+
+Lemma to_list_from_list : forall {T} (n:nat) (xs:list T) pf, to_list n (from_list n xs pf) = xs.
+Proof.
+  destruct xs; simpl; intros; subst; auto.
+  generalize dependent t. simpl in *.
+  induction xs; simpl in *; intros; congruence.
+Qed.
\ No newline at end of file
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 1f1be243e..29d745732 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -858,18 +858,17 @@ let obligation_terminator name num guard hook auto pf =
       in
       let obl = { obl with obl_status = false, status } in
       let uctx = Evd.evar_context_universe_context ctx in
-      let (def, obl) = declare_obligation prg obl body ty uctx in
+      let (_, obl) = declare_obligation prg obl body ty uctx in
       let obls = Array.copy obls in
       let _ = obls.(num) <- obl in
       try
       ignore (update_obls prg obls (pred rem));
-      if def then
-        if pred rem > 0 then
-          begin
-	    let deps = dependencies obls num in
-	    if not (Int.Set.is_empty deps) then
+      if pred rem > 0 then
+        begin
+	  let deps = dependencies obls num in
+	  if not (Int.Set.is_empty deps) then
 	    ignore (auto (Some name) None deps)
-	  end
+	end
       with e when CErrors.noncritical e ->
         let e = CErrors.push e in
         pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))