diff options
Diffstat (limited to 'vernac/obligations.ml')
| -rw-r--r-- | vernac/obligations.ml | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 6f3921903..ea2401b5c 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -144,10 +144,11 @@ let trunc_named_context n ctx = List.firstn (len - n) ctx let rec chop_product n t = + let pop t = Vars.lift (-1) t in if Int.equal n 0 then Some t else match kind_of_term t with - | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None + | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (pop b) else None | _ -> None let evar_dependencies evm oev = @@ -266,7 +267,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 + EConstr.Unsafe.to_constr (Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty (EConstr.of_constr c)) exception NoObligations of Id.t option @@ -398,7 +399,7 @@ let subst_deps expand obls deps t = (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) let rec prod_app t n = - match kind_of_term (Termops.strip_outer_cast t) with + match kind_of_term (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (** FIXME *) with | Prod (_,_,b) -> subst1 n b | LetIn (_, b, t, b') -> prod_app (subst1 b b') n | _ -> @@ -523,7 +524,7 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype = but doing it properly involves delta-reduction, and it finally doesn't seem to worth the effort (except for huge mutual fixpoints ?) *) - let m = Termops.nb_prod fixtype in + let m = Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) (** FIXME *) in let ctx = fst (decompose_prod_n_assum m fixtype) in List.map_i (fun i _ -> i) 0 ctx @@ -536,8 +537,10 @@ 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 + let term = EConstr.Unsafe.to_constr term in + let typ = EConstr.Unsafe.to_constr typ in x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l) in (* let fixdefs = List.map reduce_fix fixdefs in *) @@ -817,7 +820,7 @@ let rec string_of_list sep f = function let solve_by_tac name evi t poly ctx = let id = name in - let concl = evi.evar_concl in + let concl = EConstr.of_constr evi.evar_concl in (* spiwack: the status is dropped. *) let (entry,_,ctx') = Pfedit.build_constant_by_tactic id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in @@ -935,7 +938,7 @@ let rec solve_obligation prg num tac = Proof_global.make_terminator (obligation_terminator prg.prg_name num guard hook auto) in let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in - let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type ~terminator hook in + let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator hook in let _ = Pfedit.by !default_tactic in Option.iter (fun tac -> Pfedit.set_end_tac tac) tac |