diff options
Diffstat (limited to 'pretyping/evardefine.ml')
| -rw-r--r-- | pretyping/evardefine.ml | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 5831d3191..faf34baf7 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -11,10 +11,10 @@ open Pp open Names open Term open Termops +open Environ open EConstr open Vars open Namegen -open Environ open Evd open Evarutil open Pretype_errors @@ -22,25 +22,20 @@ open Sigma.Notations module RelDecl = Context.Rel.Declaration -let nlocal_assum (na, t) = - let open Context.Named.Declaration in - let inj = EConstr.Unsafe.to_constr in - LocalAssum (na, inj t) - let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ = let evd = Sigma.Unsafe.of_evar_map evd in let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in (Sigma.to_evar_map evd, evk) let env_nf_evar sigma env = - let nf_evar c = EConstr.Unsafe.to_constr (nf_evar sigma (EConstr.of_constr c)) in + let nf_evar c = nf_evar sigma c in process_rel_context (fun d e -> push_rel (RelDecl.map_constr nf_evar d) e) env let env_nf_betaiotaevar sigma env = process_rel_context (fun d e -> - push_rel (RelDecl.map_constr (fun c -> EConstr.Unsafe.to_constr (Reductionops.nf_betaiota sigma (EConstr.of_constr c))) d) e) env + push_rel (RelDecl.map_constr (fun c -> Reductionops.nf_betaiota sigma c) d) e) env (****************************************) (* Operations on value/type constraints *) @@ -93,7 +88,7 @@ let define_pure_evar_as_product evd evk = (Sigma.to_evar_map evd1, e) in let evd2,rng = - let newenv = push_named (nlocal_assum (id, dom)) evenv in + let newenv = push_named (LocalAssum (id, dom)) evenv in let src = evar_source evk evd1 in let filter = Filter.extend 1 (evar_filter evi) in if is_prop_sort s then @@ -146,7 +141,7 @@ let define_pure_evar_as_lambda env evd evk = let avoid = ids_of_named_context (evar_context evi) in let id = next_name_away_with_default_using_types "x" na avoid (EConstr.Unsafe.to_constr (Reductionops.whd_evar evd dom)) in - let newenv = push_named (nlocal_assum (id, dom)) evenv in + let newenv = push_named (LocalAssum (id, dom)) evenv in let filter = Filter.extend 1 (evar_filter evi) in let src = evar_source evk evd1 in let evd2,body = new_evar_unsafe newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in |