diff options
| author | Matthieu Sozeau | 2018-09-07 13:23:09 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-09-07 14:06:17 +0200 |
| commit | e3e9300a2444f5d2e595a63bf63c91e61653d77d (patch) | |
| tree | ec2e0ea492d5c4abf085385cb0b1f2797c1ff0ee /vernac | |
| parent | 07c3905c30590c93f1b173833087bbd1df364227 (diff) | |
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.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/obligations.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 *) |