diff options
| author | Pierre-Marie Pédrot | 2018-09-12 13:11:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-12 13:11:53 +0200 |
| commit | 3c7b8a7019424606cac07d50844759e2ee0e9262 (patch) | |
| tree | 047ea13e3918d3e70729e9cf9d34ee72703956ab /vernac | |
| parent | 39ca9e6931b55e63219a22a678eb6c15b0015a0f (diff) | |
| parent | e3e9300a2444f5d2e595a63bf63c91e61653d77d (diff) | |
Merge PR #8433: Fix bug #8432 : program fixpoint and universes
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 *) |