diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/class.ml | 1 | ||||
| -rw-r--r-- | vernac/himsg.ml | 20 | ||||
| -rw-r--r-- | vernac/obligations.ml | 11 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
4 files changed, 15 insertions, 19 deletions
diff --git a/vernac/class.ml b/vernac/class.ml index 59d933108..f0b01061b 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -181,6 +181,7 @@ let build_id_coercion idf_opt source poly = let sigma, vs = match source with | CL_CONST sp -> Evd.fresh_global env sigma (ConstRef sp) | _ -> error_not_transparent source in + let vs = EConstr.Unsafe.to_constr vs in let c = match constant_opt_value_in env (destConst vs) with | Some c -> c | None -> error_not_transparent source in diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 23c863cab..acb461cac 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -75,11 +75,7 @@ let rec contract3' env sigma a b c = function | MetaOccurInBody _ | InstanceNotSameType _ | ProblemBeyondCapabilities | UnifUnivInconsistency _ as x -> contract3 env sigma a b c, x | CannotSolveConstraint ((pb,env',t,u),x) -> - let t = EConstr.of_constr t in - let u = EConstr.of_constr u in let env',t,u = contract2 env' sigma t u in - let t = EConstr.Unsafe.to_constr t in - let u = EConstr.Unsafe.to_constr u in let y,x = contract3' env sigma a b c x in y,CannotSolveConstraint ((pb,env',t,u),x) @@ -322,8 +318,6 @@ let explain_unification_error env sigma p1 p2 = function else [str "universe inconsistency"] | CannotSolveConstraint ((pb,env,t,u),e) -> - let t = EConstr.of_constr t in - let u = EConstr.of_constr u in let env = make_all_name_different env sigma in (strbrk "cannot satisfy constraint " ++ pr_leconstr_env env sigma t ++ str " == " ++ pr_leconstr_env env sigma u) @@ -562,9 +556,9 @@ let rec explain_evar_kind env sigma evk ty = function | Evar_kinds.SubEvar (where,evk') -> let evi = Evd.find sigma evk' in let pc = match evi.evar_body with - | Evar_defined c -> pr_leconstr_env env sigma (EConstr.of_constr c) + | Evar_defined c -> pr_leconstr_env env sigma c | Evar_empty -> assert false in - let ty' = EConstr.of_constr evi.evar_concl in + let ty' = evi.evar_concl in (match where with | Some Evar_kinds.Body -> str "the body of " | Some Evar_kinds.Domain -> str "the domain of " @@ -577,11 +571,11 @@ let rec explain_evar_kind env sigma evk ty = function (pr_leconstr_env env sigma ty') (snd evi.evar_source) let explain_typeclass_resolution env sigma evi k = - match Typeclasses.class_of_constr sigma (EConstr.of_constr evi.evar_concl) with + match Typeclasses.class_of_constr sigma evi.evar_concl with | Some _ -> let env = Evd.evar_filtered_env evi in fnl () ++ str "Could not find an instance for " ++ - pr_lconstr_env env sigma evi.evar_concl ++ + pr_leconstr_env env sigma evi.evar_concl ++ pr_trailing_ne_context_of env sigma | _ -> mt() @@ -590,14 +584,14 @@ let explain_placeholder_kind env sigma c e = | Some (SeveralInstancesFound n) -> strbrk " (several distinct possible type class instances found)" | None -> - match Typeclasses.class_of_constr sigma (EConstr.of_constr c) with + match Typeclasses.class_of_constr sigma c with | Some _ -> strbrk " (no type class instance found)" | _ -> mt () let explain_unsolvable_implicit env sigma evk explain = let evi = Evarutil.nf_evar_info sigma (Evd.find_undefined sigma evk) in let env = Evd.evar_filtered_env evi in - let type_of_hole = pr_lconstr_env env sigma evi.evar_concl in + let type_of_hole = pr_leconstr_env env sigma evi.evar_concl in let pe = pr_trailing_ne_context_of env sigma in strbrk "Cannot infer " ++ explain_evar_kind env sigma evk type_of_hole (snd evi.evar_source) ++ @@ -765,7 +759,7 @@ let pr_constraints printenv env sigma evars cstrs = let evs = prlist (fun (ev, evi) -> fnl () ++ pr_existential_key sigma ev ++ - str " : " ++ pr_lconstr_env env' sigma evi.evar_concl ++ fnl ()) l + str " : " ++ pr_leconstr_env env' sigma evi.evar_concl ++ fnl ()) l in h 0 (pe ++ evs ++ pr_evar_constraints sigma cstrs) else diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 064e40b9b..3f2792518 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -209,8 +209,10 @@ let eterm_obligations env name evm fs ?status t ty = List.fold_right (fun (id, (n, nstr), ev) l -> let hyps = Evd.evar_filtered_context ev in - let hyps = trunc_named_context nc_len hyps in - let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in + let hyps = trunc_named_context nc_len hyps in + let hyps = EConstr.Unsafe.to_named_context hyps in + let concl = EConstr.Unsafe.to_constr ev.evar_concl in + let evtyp, deps, transp = etype_of_evar l hyps concl in let evtyp, hyps, chop = match chop_product fs evtyp with | Some t -> t, trunc_named_context fs hyps, fs @@ -356,7 +358,7 @@ let _ = optread = get_shrink_obligations; optwrite = set_shrink_obligations; } -let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type +let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type) let get_obligation_body expand obl = match obl.obl_body with @@ -813,10 +815,9 @@ let rec string_of_list sep f = function let solve_by_tac name evi t poly ctx = let id = name 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 + id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl (Tacticals.New.tclCOMPLETE t) in let env = Global.env () in let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in let body, () = Future.force entry.const_entry_body in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index b44c7cccb..a9d1631ba 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -449,7 +449,7 @@ let start_proof_and_print k l hook = let evi = Evarutil.nf_evar_info sigma evi in let env = Evd.evar_filtered_env evi in try - let concl = EConstr.of_constr evi.Evd.evar_concl in + let concl = evi.Evd.evar_concl in if not (Evarutil.is_ground_env sigma env && Evarutil.is_ground_term sigma concl) then raise Exit; |