From e3e9300a2444f5d2e595a63bf63c91e61653d77d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 7 Sep 2018 13:23:09 +0200
Subject: Fix bug #8432 : program fixpoint and universes

One didn't normalize the bodies of fixpoints according to the universe
context, resulting in a type errors. Use EConstr.to_constr to ensure
universes are normalized instead of using EConstr.Unsafe.to_constr.
---
 test-suite/bugs/closed/8432.v | 39 +++++++++++++++++++++++++++++++++++++++
 vernac/obligations.ml         |  6 +++---
 2 files changed, 42 insertions(+), 3 deletions(-)
 create mode 100644 test-suite/bugs/closed/8432.v

diff --git a/test-suite/bugs/closed/8432.v b/test-suite/bugs/closed/8432.v
new file mode 100644
index 0000000000..844ee12668
--- /dev/null
+++ b/test-suite/bugs/closed/8432.v
@@ -0,0 +1,39 @@
+Require Import Program.Tactics.
+
+Obligation Tactic := idtac.
+Set Universe Polymorphism.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Inductive Empty : Type :=.
+Inductive Unit : Type := tt.
+Definition not (A : Type) := A -> Empty.
+
+  Lemma nat_path_O_S (n : nat) (H : paths O (S n)) : Empty.
+  Proof. refine (
+    match H in paths _ i return
+      match i with
+      | O => Unit
+      | S _ => Empty
+      end
+    with
+    | idpath _ => tt
+    end
+  ). Defined.
+  Lemma symmetry {A} (x y : A) (p : paths x y) : paths y x.
+  Proof.
+    destruct p. apply idpath.
+  Defined.
+  Lemma nat_path_S_O (n : nat) (H : paths (S n) O) : Empty.
+  Proof. eapply nat_path_O_S. exact (symmetry _ _ H). Defined.
+Set Printing Universes.
+Program Fixpoint succ_not_zero (n:nat) : not (paths (S n) 0) :=
+match n as n return not (paths (S n) 0) with
+| 0 => nat_path_S_O _
+| S n' => let dummy := succ_not_zero n' in _
+end.
+Next Obligation.
+  intros f _ n dummy H. exact (nat_path_S_O _ H).
+  Show Universes.
+Defined.
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 14d7642328..3987e53bc7 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -523,11 +523,11 @@ let declare_mutual_definition l =
       (List.map (fun x -> 
 	let subs, typ = (subst_body true x) in
         let env = Global.env () in
-        let sigma = Evd.from_env env in
+        let sigma = Evd.from_ctx x.prg_ctx in
         let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in
         let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in
-	let term = EConstr.Unsafe.to_constr term in
-	let typ = EConstr.Unsafe.to_constr typ in
+        let term = EConstr.to_constr sigma term in
+        let typ = EConstr.to_constr sigma typ in
 	  x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l)
   in
 (*   let fixdefs = List.map reduce_fix fixdefs in *)
-- 
cgit v1.2.3