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.
---
 vernac/obligations.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'vernac')

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