diff options
Diffstat (limited to 'toplevel/obligations.ml')
| -rw-r--r-- | toplevel/obligations.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 1d5e4a2fa..8aee9d241 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -264,7 +264,7 @@ let pperror cmd = CErrors.user_err ~hdr:"Program" cmd let error s = pperror (str s) let reduce c = - Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty c + Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty (EConstr.of_constr c) exception NoObligations of Id.t option @@ -534,8 +534,8 @@ let declare_mutual_definition l = List.split3 (List.map (fun x -> let subs, typ = (subst_body true x) in - let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len subs) in - let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len typ) in + let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len (EConstr.of_constr subs)) in + let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len (EConstr.of_constr typ)) in x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l) in (* let fixdefs = List.map reduce_fix fixdefs in *) |