diff options
Diffstat (limited to 'vernac/himsg.ml')
| -rw-r--r-- | vernac/himsg.ml | 67 |
1 files changed, 30 insertions, 37 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 698ee4703..5d671ef52 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) @@ -90,7 +86,7 @@ let j_nf_betaiotaevar env sigma j = uj_type = Reductionops.nf_betaiota env sigma j.uj_type } let jv_nf_betaiotaevar env sigma jl = - Array.map (fun j -> j_nf_betaiotaevar env sigma j) jl + Array.Smart.map (fun j -> j_nf_betaiotaevar env sigma j) jl (** Printers *) @@ -201,7 +197,7 @@ let rec pr_disjunction pr = function let pr_puniverses f env (c,u) = f env c ++ (if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then - str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)" + str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)" else mt()) let explain_elim_arity env sigma ind sorts c pj okinds = @@ -318,12 +314,10 @@ let explain_unification_error env sigma p1 p2 = function | UnifUnivInconsistency p -> if !Constrextern.print_universes then [str "universe inconsistency: " ++ - Univ.explain_universe_inconsistency Universes.pr_with_global_universes p] + Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes p] 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) ++ @@ -640,8 +634,7 @@ let explain_refiner_cannot_generalize env sigma ty = pr_leconstr_env env sigma ty ++ str "." let explain_no_occurrence_found env sigma c id = - let c = EConstr.to_constr sigma c in - str "Found no subterm matching " ++ pr_lconstr_env env sigma c ++ + str "Found no subterm matching " ++ pr_leconstr_env env sigma c ++ str " in " ++ (match id with | Some id -> Id.print id @@ -766,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 @@ -855,9 +848,9 @@ let explain_not_match_error = function str "the body of definitions differs" | NotConvertibleTypeField (env, typ1, typ2) -> str "expected type" ++ spc () ++ - quote (Printer.safe_pr_lconstr_env env Evd.empty typ2) ++ spc () ++ + quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) typ2) ++ spc () ++ str "but found type" ++ spc () ++ - quote (Printer.safe_pr_lconstr_env env Evd.empty typ1) + quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) typ1) | NotSameConstructorNamesField -> str "constructor names differ" | NotSameInductiveNameInBlockField -> @@ -893,12 +886,12 @@ let explain_not_match_error = function str"polymorphic universe instances do not match" | IncompatibleUniverses incon -> str"the universe constraints are inconsistent: " ++ - Univ.explain_universe_inconsistency Universes.pr_with_global_universes incon + Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes incon | IncompatiblePolymorphism (env, t1, t2) -> str "conversion of polymorphic values generates additional constraints: " ++ - quote (Printer.safe_pr_lconstr_env env Evd.empty t1) ++ spc () ++ + quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t1) ++ spc () ++ str "compared to " ++ spc () ++ - quote (Printer.safe_pr_lconstr_env env Evd.empty t2) + quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t2) | IncompatibleConstraints cst -> str " the expected (polymorphic) constraints do not imply " ++ let cst = Univ.AUContext.instantiate (Univ.AUContext.instance cst) cst in @@ -1018,8 +1011,9 @@ let explain_module_internalization_error = function (* Typeclass errors *) let explain_not_a_class env c = - let c = EConstr.to_constr Evd.empty c in - pr_constr_env env Evd.empty c ++ str" is not a declared type class." + let sigma = Evd.from_env env in + let c = EConstr.to_constr sigma c in + pr_constr_env env sigma c ++ str" is not a declared type class." let explain_unbound_method env cid { CAst.v = id } = str "Unbound method name " ++ Id.print (id) ++ spc () ++ @@ -1032,14 +1026,13 @@ let pr_constr_exprs exprs = let explain_mismatched_contexts env c i j = str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++ - hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env Evd.empty j) ++ + hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env (Evd.from_env env) j) ++ fnl () ++ brk (1,1) ++ hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i) let explain_typeclass_error env = function | NotAClass c -> explain_not_a_class env c | UnboundMethod (cid, id) -> explain_unbound_method env cid id - | MismatchedContextInstance (c,i,j) -> explain_mismatched_contexts env c i j (* Refiner errors *) @@ -1094,19 +1087,19 @@ let explain_refiner_error env sigma = function (* Inductive errors *) let error_non_strictly_positive env c v = - let pc = pr_lconstr_env env Evd.empty c in - let pv = pr_lconstr_env env Evd.empty v in + let pc = pr_lconstr_env env (Evd.from_env env) c in + let pv = pr_lconstr_env env (Evd.from_env env) v in str "Non strictly positive occurrence of " ++ pv ++ str " in" ++ brk(1,1) ++ pc ++ str "." let error_ill_formed_inductive env c v = - let pc = pr_lconstr_env env Evd.empty c in - let pv = pr_lconstr_env env Evd.empty v in + let pc = pr_lconstr_env env (Evd.from_env env) c in + let pv = pr_lconstr_env env (Evd.from_env env) v in str "Not enough arguments applied to the " ++ pv ++ str " in" ++ brk(1,1) ++ pc ++ str "." let error_ill_formed_constructor env id c v nparams nargs = - let pv = pr_lconstr_env env Evd.empty v in + let pv = pr_lconstr_env env (Evd.from_env env) v in let atomic = Int.equal (nb_prod Evd.empty (EConstr.of_constr c)) (** FIXME *) 0 in str "The type of constructor" ++ brk(1,1) ++ Id.print id ++ brk(1,1) ++ str "is not valid;" ++ brk(1,1) ++ @@ -1126,12 +1119,12 @@ let error_ill_formed_constructor env id c v nparams nargs = let pr_ltype_using_barendregt_convention_env env c = (* Use goal_concl_style as an approximation of Barendregt's convention (?) *) - quote (pr_goal_concl_style_env env Evd.empty (EConstr.of_constr c)) + quote (pr_goal_concl_style_env env (Evd.from_env env) (EConstr.of_constr c)) let error_bad_ind_parameters env c n v1 v2 = let pc = pr_ltype_using_barendregt_convention_env env c in - let pv1 = pr_lconstr_env env Evd.empty v1 in - let pv2 = pr_lconstr_env env Evd.empty v2 in + let pv1 = pr_lconstr_env env (Evd.from_env env) v1 in + let pv2 = pr_lconstr_env env (Evd.from_env env) v2 in str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++ str " as " ++ pr_nth n ++ str " argument in" ++ brk(1,1) ++ pc ++ str "." @@ -1149,7 +1142,7 @@ let error_same_names_overlap idl = prlist_with_sep pr_comma Id.print idl ++ str "." let error_not_an_arity env c = - str "The type" ++ spc () ++ pr_lconstr_env env Evd.empty c ++ spc () ++ + str "The type" ++ spc () ++ pr_lconstr_env env (Evd.from_env env) c ++ spc () ++ str "is not an arity." let error_bad_entry () = @@ -1323,4 +1316,4 @@ let explain_reduction_tactic_error = function str "The abstracted term" ++ spc () ++ quote (pr_goal_concl_style_env env sigma c) ++ spc () ++ str "is not well typed." ++ fnl () ++ - explain_type_error env' Evd.empty e + explain_type_error env' (Evd.from_env env') e |