diff options
| -rw-r--r-- | engine/proofview.ml | 2 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 3 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 4 | ||||
| -rw-r--r-- | tactics/autorewrite.ml | 22 | ||||
| -rw-r--r-- | tactics/eqschemes.ml | 11 | ||||
| -rw-r--r-- | tactics/inv.ml | 2 | ||||
| -rw-r--r-- | tactics/leminv.ml | 5 | ||||
| -rw-r--r-- | vernac/comInductive.ml | 3 |
8 files changed, 28 insertions, 24 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index fdb0a215d..b4afb6415 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -39,7 +39,7 @@ let proofview p = let compact el ({ solution } as pv) = let nf c = Evarutil.nf_evar solution c in - let nf0 c = EConstr.Unsafe.to_constr (Evarutil.nf_evar solution (EConstr.of_constr c)) in + let nf0 c = EConstr.(to_constr solution (of_constr c)) in let size = Evd.fold (fun _ _ i -> i+1) solution 0 in let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in let pruned_solution = Evd.drop_all_defined solution in diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 03c0969fa..678c3ea3f 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -200,8 +200,7 @@ let refine_by_tactic env sigma ty tac = | [c, _] -> c | _ -> assert false in - let ans = Reductionops.nf_evar sigma ans in - let ans = EConstr.Unsafe.to_constr ans in + let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in (** [neff] contains the freshly generated side-effects *) let neff = Evd.eval_side_effects sigma in (** Reset the old side-effects *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 3abdd129e..946379356 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -437,8 +437,8 @@ let return_proof ?(allow_partial=false) () = (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) - let proofs = - List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr c), eff)) initial_goals in + let proofs = + List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in proofs, Evd.evar_universe_context evd let close_future_proof ~feedback_id proof = diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 0b0e629ab..c8fd0b7a7 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -228,7 +228,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = if metas then eqclause else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd) in - let (equiv, args) = decompose_app (EConstr.Unsafe.to_constr (Clenv.clenv_type eqclause)) in + let (equiv, args) = EConstr.decompose_app sigma (Clenv.clenv_type eqclause) in let rec split_last_two = function | [c1;c2] -> [],(c1, c2) | x::y::z -> @@ -236,17 +236,19 @@ let decompose_applied_relation metas env sigma c ctype left2right = | _ -> raise Not_found in try - let others,(c1,c2) = split_last_two args in - let ty1, ty2 = - Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c1), Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c2) - in - let ty = EConstr.Unsafe.to_constr ty in - let ty1 = EConstr.Unsafe.to_constr ty1 in + let others,(c1,c2) = split_last_two args in + let ty1, ty2 = Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 in + (* XXX: It looks like mk_clenv_from_env should be fixed instead? *) + let open EConstr in + let hyp_ty = Unsafe.to_constr ty in + let hyp_car = Unsafe.to_constr ty1 in + let hyp_prf = Unsafe.to_constr @@ Clenv.clenv_value eqclause in + let hyp_rel = Unsafe.to_constr @@ mkApp (equiv, Array.of_list others) in + let hyp_left = Unsafe.to_constr @@ c1 in + let hyp_right = Unsafe.to_constr @@ c2 in (* if not (evd_convertible env eqclause.evd ty1 ty2) then None *) (* else *) - Some { hyp_cl=eqclause; hyp_prf=EConstr.Unsafe.to_constr (Clenv.clenv_value eqclause); hyp_ty = ty; - hyp_car=ty1; hyp_rel=mkApp (equiv, Array.of_list others); - hyp_l2r=left2right; hyp_left=c1; hyp_right=c2; } + Some { hyp_cl=eqclause; hyp_prf; hyp_ty; hyp_car; hyp_rel; hyp_l2r=left2right; hyp_left; hyp_right; } with Not_found -> None in match find_rel ctype with diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index eede13329..ad5239116 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -108,9 +108,14 @@ let get_coq_eq ctx = user_err Pp.(str "eq not found.") let univ_of_eq env eq = - let eq = EConstr.of_constr eq in - match Constr.kind (EConstr.Unsafe.to_constr (Retyping.get_type_of env (Evd.from_env env) eq)) with - | Prod (_,t,_) -> (match Constr.kind t with Sort (Type u) -> u | _ -> assert false) + let open EConstr in + let eq = of_constr eq in + let sigma = Evd.from_env env in + match kind sigma (Retyping.get_type_of env sigma eq) with + | Prod (_,t,_) -> (match kind sigma t with + Sort k -> + (match ESorts.kind sigma k with Type u -> u | _ -> assert false) + | _ -> assert false) | _ -> assert false (**********************************************************************) diff --git a/tactics/inv.ml b/tactics/inv.ml index 339abbc2e..102b8e54d 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -293,7 +293,7 @@ let error_too_many_names pats = str "Unexpected " ++ str (String.plural (List.length pats) "introduction pattern") ++ str ": " ++ pr_enum (Miscprint.pr_intro_pattern - (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env (Evd.from_env env)))))) pats ++ + (fun c -> Printer.pr_econstr_env env sigma (snd (c env (Evd.from_env env))))) pats ++ str ".") let get_names (allow_conj,issimple) ({CAst.loc;v=pat} as x) = match pat with diff --git a/tactics/leminv.ml b/tactics/leminv.ml index f47e6b2cd..10937322e 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -232,9 +232,8 @@ let inversion_scheme env sigma t sort dep_option inv_op = let c = fill_holes pfterm in (* warning: side-effect on ownSign *) let invProof = it_mkNamedLambda_or_LetIn c !ownSign in - let invProof = EConstr.Unsafe.to_constr invProof in - let p = Evarutil.nf_evars_universes sigma invProof in - p, sigma + let p = EConstr.to_constr sigma invProof in + p, sigma let add_inversion_lemma ~poly name env sigma t sort dep inv_op = let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 101c14266..b93e8d9ac 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -27,7 +27,6 @@ open Impargs open Reductionops open Indtypes open Pretyping -open Evarutil open Indschemes open Context.Rel.Declaration open Entries @@ -158,7 +157,7 @@ let sign_level env evd sign = | LocalDef _ -> lev, push_rel d env | LocalAssum _ -> let s = destSort (Reduction.whd_all env - (EConstr.Unsafe.to_constr (nf_evar evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d)))))) + (EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d))))) in let u = univ_of_sort s in (Univ.sup u lev, push_rel d env)) |