From 4bc936b22f9ed1e90286f39c8d51c9f05c37b300 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Apr 2014 12:59:16 +0200
Subject: Fix program Fixpoint not taking care of universes.

---
 toplevel/command.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 4a26b75022..f21c1b30d7 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -838,9 +838,11 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
 	  [| argtyp ; wf_rel ;
 	     Evarutil.e_new_evar evdref env 
 	       ~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
-	     prop ; intern_body_lam |])
+	     prop |])
   in
+  let def = Typing.solve_evars env evdref def in
   let _ = evdref := Evarutil.nf_evar_map !evdref in
+  let def = mkApp (def, [|intern_body_lam|]) in
   let binders_rel = nf_evar_context !evdref binders_rel in
   let binders = nf_evar_context !evdref binders in
   let top_arity = Evarutil.nf_evar !evdref top_arity in
-- 
cgit v1.2.3