From 9f5e248704f1574b0acbb9bddd287e40daac8727 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 27 Jul 2016 18:26:42 +0200
Subject: Fix bug #3886, generation of obligations of fixes

This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1
---
 test-suite/bugs/closed/3886.v | 23 +++++++++++++++++++++++
 toplevel/command.ml           |  8 +++++++-
 2 files changed, 30 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/3886.v

diff --git a/test-suite/bugs/closed/3886.v b/test-suite/bugs/closed/3886.v
new file mode 100644
index 0000000000..2ac4abe54f
--- /dev/null
+++ b/test-suite/bugs/closed/3886.v
@@ -0,0 +1,23 @@
+Require Import Program.
+
+Inductive Even : nat -> Prop :=
+| evenO : Even O
+| evenS : forall n, Odd n -> Even (S n)
+with Odd : nat -> Prop :=
+| oddS : forall n, Even n -> Odd (S n).
+
+Program Fixpoint doubleE {n} (e : Even n) : Even (2 * n)
+  := _
+with doubleO {n} (o : Odd n) : Odd (S (2 * n))
+     := _.
+Obligations.
+Axiom cheat : forall {A}, A.
+Obligation 1 of doubleE.
+apply cheat.
+Qed.
+
+Obligation 1 of doubleO.
+apply cheat.
+Qed.
+
+Check doubleE.
\ No newline at end of file
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 8eb2232eda..b9e4dbd7b2 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1222,6 +1222,11 @@ let out_def = function
   | Some def -> def
   | None -> error "Program Fixpoint needs defined bodies."
 
+let collect_evars_of_term evd c ty =
+  let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in
+  Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
+  evars (Evd.from_ctx (Evd.evar_universe_context evd))
+
 let do_program_recursive local p fixkind fixl ntns =
   let isfix = fixkind != Obligations.IsCoFixpoint in
   let (env, rec_sign, pl, evd), fix, info = 
@@ -1239,8 +1244,9 @@ let do_program_recursive local p fixkind fixl ntns =
     and typ =
       nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign)
     in
+    let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ = 
-      Obligations.eterm_obligations env id evd
+      Obligations.eterm_obligations env id evm
 	(List.length rec_sign) def typ
     in (id, def, typ, imps, evars)
   in
-- 
cgit v1.2.3