diff options
| author | Matthieu Sozeau | 2014-04-07 12:59:16 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:59 +0200 |
| commit | 4bc936b22f9ed1e90286f39c8d51c9f05c37b300 (patch) | |
| tree | 30bcfa44115d7fec8df4824aaba336a384c8e58f | |
| parent | 105db906ae45e792d1caeeb2e3fb7f69944b2caa (diff) | |
Fix program Fixpoint not taking care of universes.
| -rw-r--r-- | toplevel/command.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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 |