aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/top_printers.ml2
-rw-r--r--plugins/subtac/subtac.ml2
-rw-r--r--pretyping/pretype_errors.ml79
-rw-r--r--pretyping/pretype_errors.mli41
-rw-r--r--pretyping/unification.ml12
-rw-r--r--proofs/clenv.ml2
-rw-r--r--proofs/logic.ml6
-rw-r--r--proofs/proofview.ml7
-rw-r--r--tactics/equality.ml6
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--tactics/rewrite.ml42
-rw-r--r--tactics/tactics.ml4
-rw-r--r--toplevel/cerrors.ml6
-rw-r--r--toplevel/himsg.ml95
-rw-r--r--toplevel/himsg.mli4
-rw-r--r--toplevel/vernacentries.ml4
16 files changed, 141 insertions, 133 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 7b1fba0110..7af0a357ab 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -57,7 +57,7 @@ let ppsconstr x = ppconstr (Declarations.force x)
let ppconstr_univ x = Constrextern.with_universes ppconstr x
let pprawconstr = (fun x -> pp(pr_lrawconstr x))
let pppattern = (fun x -> pp(pr_constr_pattern x))
-let pptype = (fun x -> pp(pr_ltype x))
+let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e)))
let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 4a244553ee..62fa0b2c9f 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -218,7 +218,7 @@ let subtac (loc, command) =
| Type_errors.TypeError (env, exn) as e -> raise e
- | Pretype_errors.PretypeError (env, exn) as e -> raise e
+ | Pretype_errors.PretypeError (env, _, exn) as e -> raise e
| (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
Loc.Exc_located (loc, e') as e) -> raise e
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index eb07addb07..cd2ed76c1f 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -38,8 +38,9 @@ type pretype_error =
| VarNotFound of identifier
| UnexpectedType of constr * constr
| NotProduct of constr
+ | TypingError of type_error
-exception PretypeError of env * pretype_error
+exception PretypeError of env * Evd.evar_map * pretype_error
let precatchable_exception = function
| Util.UserError _ | TypeError _ | PretypeError _
@@ -55,13 +56,13 @@ let j_nf_betaiotaevar sigma j =
{ uj_val = nf_evar sigma j.uj_val;
uj_type = Reductionops.nf_betaiota sigma j.uj_type }
let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl
-let jl_nf_betaiotaevar sigma jl =
- List.map (j_nf_betaiotaevar sigma) jl
+let jv_nf_betaiotaevar sigma jl =
+ Array.map (j_nf_betaiotaevar sigma) jl
let jv_nf_evar sigma = Array.map (j_nf_evar sigma)
let tj_nf_evar sigma {utj_val=v;utj_type=t} =
{utj_val=nf_evar sigma v;utj_type=t}
-let env_ise sigma env =
+let env_nf_evar sigma env =
let sign = named_context_val env in
let ctxt = rel_context env in
let env0 = reset_with_named_context sign env in
@@ -97,110 +98,90 @@ let contract2 env a b = match contract env [a;b] with
let contract3 env a b c = match contract env [a;b;c] with
| env, [a;b;c] -> env,a,b,c | _ -> assert false
-let raise_pretype_error (loc,ctx,sigma,te) =
- Loc.raise loc (PretypeError(env_ise sigma ctx,te))
+let raise_pretype_error (loc,env,sigma,te) =
+ Loc.raise loc (PretypeError(env,sigma,te))
-let raise_located_type_error (loc,ctx,sigma,te) =
- Loc.raise loc (TypeError(env_ise sigma ctx,te))
+let raise_located_type_error (loc,env,sigma,te) =
+ Loc.raise loc (PretypeError(env,sigma,TypingError te))
let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty =
let env, c, actty, expty = contract3 env c actty expty in
- let j = j_nf_evar sigma {uj_val=c;uj_type=actty} in
- raise_located_type_error
- (loc, env, sigma, ActualType (j, nf_evar sigma expty))
+ let j = {uj_val=c;uj_type=actty} in
+ raise_located_type_error (loc, env, sigma, ActualType (j, expty))
let error_cant_apply_not_functional_loc loc env sigma rator randl =
- let ja = Array.of_list (jl_nf_evar sigma randl) in
raise_located_type_error
- (loc, env, sigma,
- CantApplyNonFunctional (j_nf_evar sigma rator, ja))
+ (loc, env, sigma, CantApplyNonFunctional (rator, Array.of_list randl))
let error_cant_apply_bad_type_loc loc env sigma (n,c,t) rator randl =
- let ja = Array.of_list (jl_nf_betaiotaevar sigma randl) in
raise_located_type_error
(loc, env, sigma,
- CantApplyBadType
- ((n,nf_evar sigma c, Reductionops.nf_betaiota sigma t),
- j_nf_evar sigma rator, ja))
+ CantApplyBadType ((n,c,t), rator, Array.of_list randl))
let error_ill_formed_branch_loc loc env sigma c i actty expty =
- let simp t = Reduction.nf_betaiota (nf_evar sigma t) in
raise_located_type_error
- (loc, env, sigma,
- IllFormedBranch (nf_evar sigma c,i,simp actty, simp expty))
+ (loc, env, sigma, IllFormedBranch (c, i, actty, expty))
let error_number_branches_loc loc env sigma cj expn =
- raise_located_type_error
- (loc, env, sigma,
- NumberBranches (j_nf_evar sigma cj, expn))
+ raise_located_type_error (loc, env, sigma, NumberBranches (cj, expn))
let error_case_not_inductive_loc loc env sigma cj =
- raise_located_type_error
- (loc, env, sigma, CaseNotInductive (j_nf_evar sigma cj))
+ raise_located_type_error (loc, env, sigma, CaseNotInductive cj)
let error_ill_typed_rec_body_loc loc env sigma i na jl tys =
raise_located_type_error
- (loc, env, sigma,
- IllTypedRecBody (i,na,jv_nf_evar sigma jl,
- Array.map (nf_evar sigma) tys))
+ (loc, env, sigma, IllTypedRecBody (i, na, jl, tys))
let error_not_a_type_loc loc env sigma j =
- raise_located_type_error (loc, env, sigma, NotAType (j_nf_evar sigma j))
+ raise_located_type_error (loc, env, sigma, NotAType j)
(*s Implicit arguments synthesis errors. It is hard to find
a precise location. *)
let error_occur_check env sigma ev c =
- let c = nf_evar sigma c in
- raise (PretypeError (env_ise sigma env, OccurCheck (ev,c)))
+ raise (PretypeError (env, sigma, OccurCheck (ev,c)))
let error_not_clean env sigma ev c (loc,k) =
- let c = nf_evar sigma c in
- Loc.raise loc
- (PretypeError (env_ise sigma env, NotClean (ev,c,k)))
+ Loc.raise loc (PretypeError (env, sigma, NotClean (ev,c,k)))
let error_unsolvable_implicit loc env sigma evi e explain =
Loc.raise loc
- (PretypeError (env_ise sigma env, UnsolvableImplicit (evi, e, explain)))
+ (PretypeError (env, sigma, UnsolvableImplicit (evi, e, explain)))
let error_cannot_unify env sigma (m,n) =
- let m = nf_evar sigma m and n = nf_evar sigma n in
- raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
+ raise (PretypeError (env, sigma,CannotUnify (m,n)))
let error_cannot_unify_local env sigma (m,n,sn) =
- raise (PretypeError (env_ise sigma env,CannotUnifyLocal (m,n,sn)))
+ raise (PretypeError (env, sigma,CannotUnifyLocal (m,n,sn)))
let error_cannot_coerce env sigma (m,n) =
- raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
+ raise (PretypeError (env, sigma,CannotUnify (m,n)))
let error_cannot_find_well_typed_abstraction env sigma p l =
- raise (PretypeError (env_ise sigma env,CannotFindWellTypedAbstraction (p,l)))
+ raise (PretypeError (env, sigma,CannotFindWellTypedAbstraction (p,l)))
let error_abstraction_over_meta env sigma hdmeta metaarg =
let m = Evd.meta_name sigma hdmeta and n = Evd.meta_name sigma metaarg in
- raise (PretypeError (env_ise sigma env,AbstractionOverMeta (m,n)))
+ raise (PretypeError (env, sigma,AbstractionOverMeta (m,n)))
let error_non_linear_unification env sigma hdmeta t =
let m = Evd.meta_name sigma hdmeta in
- raise (PretypeError (env_ise sigma env,NonLinearUnification (m,t)))
+ raise (PretypeError (env, sigma,NonLinearUnification (m,t)))
(*s Ml Case errors *)
let error_cant_find_case_type_loc loc env sigma expr =
- raise_pretype_error
- (loc, env, sigma, CantFindCaseType (nf_evar sigma expr))
+ raise_pretype_error (loc, env, sigma, CantFindCaseType expr)
(*s Pretyping errors *)
let error_unexpected_type_loc loc env sigma actty expty =
let env, actty, expty = contract2 env actty expty in
- raise_pretype_error
- (loc, env, sigma,
- UnexpectedType (nf_evar sigma actty, nf_evar sigma expty))
+ raise_pretype_error (loc, env, sigma, UnexpectedType (actty, expty))
let error_not_product_loc loc env sigma c =
- raise_pretype_error (loc, env, sigma, NotProduct (nf_evar sigma c))
+ raise_pretype_error (loc, env, sigma, NotProduct c)
(*s Error in conversion from AST to rawterms *)
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index d81adb6b01..cdf6b523c9 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -37,47 +37,48 @@ type pretype_error =
| VarNotFound of identifier
| UnexpectedType of constr * constr
| NotProduct of constr
+ | TypingError of Type_errors.type_error
-exception PretypeError of env * pretype_error
+exception PretypeError of env * Evd.evar_map * pretype_error
val precatchable_exception : exn -> bool
(** Presenting terms without solved evars *)
-val nf_evar : Evd.evar_map -> constr -> constr
-val j_nf_evar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment
-val jl_nf_evar :
- Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list
-val jv_nf_evar :
- Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
-val tj_nf_evar :
- Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
+val nf_evar : Evd.evar_map -> constr -> constr
+val j_nf_evar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment
+val jl_nf_evar : Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list
+val jv_nf_evar : Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
+val tj_nf_evar : Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
+val env_nf_evar : Evd.evar_map -> env -> env
+val jv_nf_betaiotaevar :
+ Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
(** Raising errors *)
val error_actual_type_loc :
- loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b
+ loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b
val error_cant_apply_not_functional_loc :
- loc -> env -> Evd.evar_map ->
+ loc -> env -> Evd.evar_map ->
unsafe_judgment -> unsafe_judgment list -> 'b
val error_cant_apply_bad_type_loc :
- loc -> env -> Evd.evar_map -> int * constr * constr ->
+ loc -> env -> Evd.evar_map -> int * constr * constr ->
unsafe_judgment -> unsafe_judgment list -> 'b
val error_case_not_inductive_loc :
- loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b
+ loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b
val error_ill_formed_branch_loc :
- loc -> env -> Evd.evar_map ->
+ loc -> env -> Evd.evar_map ->
constr -> int -> constr -> constr -> 'b
val error_number_branches_loc :
- loc -> env -> Evd.evar_map ->
+ loc -> env -> Evd.evar_map ->
unsafe_judgment -> int -> 'b
val error_ill_typed_rec_body_loc :
- loc -> env -> Evd.evar_map ->
+ loc -> env -> Evd.evar_map ->
int -> name array -> unsafe_judgment array -> types array -> 'b
val error_not_a_type_loc :
@@ -87,7 +88,7 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
(** {6 Implicit arguments synthesis errors } *)
-val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b
+val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b
val error_not_clean :
env -> Evd.evar_map -> existential_key -> constr -> loc * Evd.hole_kind -> 'b
@@ -112,15 +113,15 @@ val error_non_linear_unification : env -> Evd.evar_map ->
(** {6 Ml Case errors } *)
val error_cant_find_case_type_loc :
- loc -> env -> Evd.evar_map -> constr -> 'b
+ loc -> env -> Evd.evar_map -> constr -> 'b
(** {6 Pretyping errors } *)
val error_unexpected_type_loc :
- loc -> env -> Evd.evar_map -> constr -> constr -> 'b
+ loc -> env -> Evd.evar_map -> constr -> constr -> 'b
val error_not_product_loc :
- loc -> env -> Evd.evar_map -> constr -> 'b
+ loc -> env -> Evd.evar_map -> constr -> 'b
(** {6 Error in conversion from AST to rawterms } *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 38cf59bc0d..6c17567c31 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -844,7 +844,7 @@ let w_unify_to_subterm env ?(flags=default_unify_flags) (op,cl) evd =
in
try matchrec cl
with ex when precatchable_exception ex ->
- raise (PretypeError (env,NoOccurrenceFound (op, None)))
+ raise (PretypeError (env,evd,NoOccurrenceFound (op, None)))
(* Tries to find all instances of term [cl] in term [op].
Unifies [cl] to every subterm of [op] and return all the matches.
@@ -906,7 +906,7 @@ let w_unify_to_subterm_all env ?(flags=default_unify_flags) (op,cl) evd =
in
let res = matchrec cl [] in
if res = [] then
- raise (PretypeError (env,NoOccurrenceFound (op, None)))
+ raise (PretypeError (env,evd,NoOccurrenceFound (op, None)))
else
res
@@ -922,7 +922,7 @@ let w_unify_to_subterm_list env flags allow_K hdmeta oplist t evd =
try
(* This is up to delta for subterms w/o metas ... *)
w_unify_to_subterm env ~flags (strip_outer_cast op,t) evd
- with PretypeError (env,NoOccurrenceFound _) when allow_K -> (evd,op)
+ with PretypeError (env,_,NoOccurrenceFound _) when allow_K -> (evd,op)
in
if not allow_K && (* ensure we found a different instance *)
List.exists (fun op -> eq_constr op cl) l
@@ -932,7 +932,7 @@ let w_unify_to_subterm_list env flags allow_K hdmeta oplist t evd =
(evd,op::l)
else
(* This is not up to delta ... *)
- raise (PretypeError (env,NoOccurrenceFound (op, None))))
+ raise (PretypeError (env,evd,NoOccurrenceFound (op, None))))
oplist
(evd,[])
@@ -996,13 +996,13 @@ let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
with ex when precatchable_exception ex ->
try
w_unify2 env flags allow_K cv_pb ty1 ty2 evd
- with PretypeError (env,NoOccurrenceFound _) as e -> raise e)
+ with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e)
(* Second order case *)
| (Meta _, true, _, _ | _, _, Meta _, true) ->
(try
w_unify2 env flags allow_K cv_pb ty1 ty2 evd
- with PretypeError (env,NoOccurrenceFound _) as e -> raise e
+ with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e
| ex when precatchable_exception ex ->
try
w_typed_unify env cv_pb flags ty1 ty2 evd
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 70f2f6b64a..71d952caf9 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -448,7 +448,7 @@ let clenv_unify_binding_type clenv c t u =
let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
TypeProcessed, { clenv with evd = evd }, c
with
- | PretypeError (_,NotClean _) as e -> raise e
+ | PretypeError (_,_,NotClean _) as e -> raise e
| e when precatchable_exception e ->
TypeNotProcessed, clenv, c
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 593ef0b329..5b55e1c02f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -48,13 +48,13 @@ open Pretype_errors
let rec catchable_exception = function
| Loc.Exc_located(_,e) -> catchable_exception e
| LtacLocated(_,e) -> catchable_exception e
- | Util.UserError _ | TypeError _
+ | Util.UserError _ | TypeError _ | PretypeError (_,_,TypingError _)
| RefinerError _ | Indrec.RecursionSchemeError _
- | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _)
+ | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _)
(* reduction errors *)
| Tacred.ReductionTacticError _
(* unification errors *)
- | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
+ | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
|NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
|CannotFindWellTypedAbstraction _|OccurCheck _
|UnsolvableImplicit _)) -> true
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 677c739428..2802acfc1a 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -395,11 +395,12 @@ let rec tclGOALBINDU s k =
open Pretype_errors
let rec catchable_exception = function
| Loc.Exc_located(_,e) -> catchable_exception e
- | Util.UserError _ | Type_errors.TypeError _
+ | Util.UserError _
+ | Type_errors.TypeError _ | PretypeError (_,_,TypingError _)
| Indrec.RecursionSchemeError _
- | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _)
+ | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _)
(* unification errors *)
- | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
+ | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
|NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
|CannotFindWellTypedAbstraction _
|UnsolvableImplicit _)) -> true
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0ed754f6f8..0144fbb34c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -134,10 +134,10 @@ let general_elim_clause with_evars cls rew elim =
an extra condition *)
tclNOTSAMEGOAL (rewrite_elim with_evars rew elim ~allow_K:false)
| Some id -> rewrite_elim_in with_evars id rew elim)
- with Pretype_errors.PretypeError (env,
- (Pretype_errors.NoOccurrenceFound (c', _))) ->
+ with Pretype_errors.PretypeError (env,evd,
+ Pretype_errors.NoOccurrenceFound (c', _)) ->
raise (Pretype_errors.PretypeError
- (env, (Pretype_errors.NoOccurrenceFound (c', cls))))
+ (env,evd,Pretype_errors.NoOccurrenceFound (c', cls)))
let general_elim_clause with_evars tac cls sigma c t l l2r elim gl =
let all, firstonly, tac =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 0490f1bc89..f9c8e47fd7 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -578,7 +578,7 @@ let hResolve id c occ t gl =
try
Pretyping.Default.understand sigma env t_hole
with
- | Loc.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) ->
+ | Loc.Exc_located (loc,Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _)) ->
resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole)
in
let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 99cbfe4980..860f162dbc 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1532,7 +1532,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
with RewriteFailure ->
let {l2r=l2r; c1=x; c2=y} = hypinfo in
raise (Pretype_errors.PretypeError
- (pf_env gl,
+ (pf_env gl,project gl,
Pretype_errors.NoOccurrenceFound ((if l2r then x else y), cl)))
let general_s_rewrite_clause x =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d18b540de7..2c4201f99f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -787,9 +787,9 @@ let simplest_elim c = default_elim false (c,NoBindings)
let clenv_fchain_in id elim_flags mv elimclause hypclause =
try clenv_fchain ~allow_K:false ~flags:elim_flags mv elimclause hypclause
- with PretypeError (env,NoOccurrenceFound (op,_)) ->
+ with PretypeError (env,evd,NoOccurrenceFound (op,_)) ->
(* Set the hypothesis name in the message *)
- raise (PretypeError (env,NoOccurrenceFound (op,Some id)))
+ raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
let elimination_in_clause_scheme with_evars id i elimclause indclause gl =
let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 68483f5e24..a497aad593 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -103,9 +103,9 @@ let rec process_vernac_interp_error = function
mt() in
wrap_vernac_error (str "Universe inconsistency" ++ msg ++ str ".")
| TypeError(ctx,te) ->
- wrap_vernac_error (Himsg.explain_type_error ctx te)
- | PretypeError(ctx,te) ->
- wrap_vernac_error (Himsg.explain_pretype_error ctx te)
+ wrap_vernac_error (Himsg.explain_type_error ctx Evd.empty te)
+ | PretypeError(ctx,sigma,te) ->
+ wrap_vernac_error (Himsg.explain_pretype_error ctx sigma te)
| Typeclasses_errors.TypeClassError(env, te) ->
wrap_vernac_error (Himsg.explain_typeclass_error env te)
| InductiveError e ->
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 191014c0b3..01eca8cb21 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -50,7 +50,8 @@ let explain_unbound_var env v =
let var = pr_id v in
str "No such section variable or assumption: " ++ var ++ str "."
-let explain_not_type env j =
+let explain_not_type env sigma j =
+ let j = j_nf_evar sigma j in
let pe = pr_ne_context_of (str "In environment") env in
let pc,pt = pr_ljudge_env env j in
pe ++ str "The term" ++ brk(1,1) ++ pc ++ spc () ++
@@ -109,7 +110,8 @@ let explain_elim_arity env ind sorts c pj okinds =
str "in the inductive type" ++ spc () ++ quote pi ++ str ":") ++
fnl () ++ msg
-let explain_case_not_inductive env cj =
+let explain_case_not_inductive env sigma cj =
+ let cj = j_nf_evar sigma cj in
let env = make_all_name_different env in
let pc = pr_lconstr_env env cj.uj_val in
let pct = pr_lconstr_env env cj.uj_type in
@@ -121,7 +123,8 @@ let explain_case_not_inductive env cj =
str "has type" ++ brk(1,1) ++ pct ++ spc () ++
str "which is not a (co-)inductive type."
-let explain_number_branches env cj expn =
+let explain_number_branches env sigma cj expn =
+ let cj = j_nf_evar sigma cj in
let env = make_all_name_different env in
let pc = pr_lconstr_env env cj.uj_val in
let pct = pr_lconstr_env env cj.uj_type in
@@ -129,11 +132,13 @@ let explain_number_branches env cj expn =
str "of type" ++ brk(1,1) ++ pct ++ spc () ++
str "expects " ++ int expn ++ str " branches."
-let explain_ill_formed_branch env c i actty expty =
+let explain_ill_formed_branch env sigma c i actty expty =
+ let simp t = Reduction.nf_betaiota (nf_evar sigma t) in
+ let c = nf_evar sigma c in
let env = make_all_name_different env in
let pc = pr_lconstr_env env c in
- let pa = pr_lconstr_env env actty in
- let pe = pr_lconstr_env env expty in
+ let pa = pr_lconstr_env env (simp actty) in
+ let pe = pr_lconstr_env env (simp expty) in
str "In pattern-matching on term" ++ brk(1,1) ++ pc ++
spc () ++ str "the " ++ nth (i+1) ++ str " branch has type" ++
brk(1,1) ++ pa ++ spc () ++
@@ -148,7 +153,9 @@ let explain_generalization env (name,var) j =
str "it has type" ++ spc () ++ pt ++
spc () ++ str "which should be Set, Prop or Type."
-let explain_actual_type env j pt =
+let explain_actual_type env sigma j pt =
+ let j = j_nf_evar sigma j in
+ let pt = nf_evar sigma pt in
let pe = pr_ne_context_of (str "In environment") env in
let (pc,pct) = pr_ljudge_env env j in
let pt = pr_lconstr_env env pt in
@@ -157,7 +164,11 @@ let explain_actual_type env j pt =
str "has type" ++ brk(1,1) ++ pct ++ brk(1,1) ++
str "while it is expected to have type" ++ brk(1,1) ++ pt ++ str "."
-let explain_cant_apply_bad_type env (n,exptyp,actualtyp) rator randl =
+let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
+ let randl = jv_nf_betaiotaevar sigma randl in
+ let exptyp = nf_evar sigma exptyp in
+ let actualtyp = Reductionops.nf_betaiota sigma actualtyp in
+ let rator = j_nf_evar sigma rator in
let env = make_all_name_different env in
let nargs = Array.length randl in
(* let pe = pr_ne_context_of (str "in environment") env in*)
@@ -179,7 +190,9 @@ let explain_cant_apply_bad_type env (n,exptyp,actualtyp) rator randl =
str "which should be coercible to" ++ brk(1,1) ++
pr_lconstr_env env exptyp ++ str "."
-let explain_cant_apply_not_functional env rator randl =
+let explain_cant_apply_not_functional env sigma rator randl =
+ let randl = jv_nf_evar sigma randl in
+ let rator = j_nf_evar sigma rator in
let env = make_all_name_different env in
let nargs = Array.length randl in
(* let pe = pr_ne_context_of (str "in environment") env in*)
@@ -198,13 +211,16 @@ let explain_cant_apply_not_functional env rator randl =
str "cannot be applied to the " ++ str (plural nargs "term") ++ fnl () ++
str " " ++ v 0 appl
-let explain_unexpected_type env actual_type expected_type =
+let explain_unexpected_type env sigma actual_type expected_type =
+ let actual_type = nf_evar sigma actual_type in
+ let expected_type = nf_evar sigma expected_type in
let pract = pr_lconstr_env env actual_type in
let prexp = pr_lconstr_env env expected_type in
str "Found type" ++ spc () ++ pract ++ spc () ++
str "where" ++ spc () ++ prexp ++ str " was expected."
-let explain_not_product env c =
+let explain_not_product env sigma c =
+ let c = nf_evar sigma c in
let pr = pr_lconstr_env env c in
str "The type of this term is a product" ++ spc () ++
str "while it is expected to be" ++
@@ -293,7 +309,9 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj =
str"Recursive definition is:" ++ spc () ++ pvd ++ str "."
with _ -> mt ())
-let explain_ill_typed_rec_body env i names vdefj vargs =
+let explain_ill_typed_rec_body env sigma i names vdefj vargs =
+ let vdefj = jv_nf_evar sigma vdefj in
+ let vargs = Array.map (nf_evar sigma) vargs in
let env = make_all_name_different env in
let pvd,pvdt = pr_ljudge_env env (vdefj.(i)) in
let pv = pr_lconstr_env env vargs.(i) in
@@ -303,12 +321,14 @@ let explain_ill_typed_rec_body env i names vdefj vargs =
str "has type" ++ spc () ++ pvdt ++ spc () ++
str "while it should be" ++ spc () ++ pv ++ str "."
-let explain_cant_find_case_type env c =
+let explain_cant_find_case_type env sigma c =
+ let c = nf_evar sigma c in
let env = make_all_name_different env in
let pe = pr_lconstr_env env c in
str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe ++ str "."
-let explain_occur_check env ev rhs =
+let explain_occur_check env sigma ev rhs =
+ let rhs = nf_evar sigma rhs in
let env = make_all_name_different env in
let id = Evd.string_of_existential ev in
let pt = pr_lconstr_env env rhs in
@@ -352,7 +372,8 @@ let explain_hole_kind env evi = function
| MatchingVar _ ->
assert false
-let explain_not_clean env ev t k =
+let explain_not_clean env sigma ev t k =
+ let t = nf_evar sigma t in
let env = make_all_name_different env in
let id = Evd.string_of_existential ev in
let var = pr_lconstr_env env t in
@@ -399,13 +420,15 @@ let explain_wrong_case_info env ind ci =
str "was given to a pattern-matching expression on the inductive type" ++
spc () ++ pc ++ str "."
-let explain_cannot_unify env m n =
+let explain_cannot_unify env sigma m n =
+ let m = nf_evar sigma m in
+ let n = nf_evar sigma n in
let pm = pr_lconstr_env env m in
let pn = pr_lconstr_env env n in
str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++
str "with" ++ brk(1,1) ++ pn ++ str "."
-let explain_cannot_unify_local env m n subn =
+let explain_cannot_unify_local env sigma m n subn =
let pm = pr_lconstr_env env m in
let pn = pr_lconstr_env env n in
let psubn = pr_lconstr_env env subn in
@@ -447,7 +470,7 @@ let explain_non_linear_unification env m t =
strbrk " which would require to abstract twice on " ++
pr_lconstr_env env t ++ str "."
-let explain_type_error env err =
+let explain_type_error env sigma err =
let env = make_all_name_different env in
match err with
| UnboundRel n ->
@@ -455,7 +478,7 @@ let explain_type_error env err =
| UnboundVar v ->
explain_unbound_var env v
| NotAType j ->
- explain_not_type env j
+ explain_not_type env sigma j
| BadAssumption c ->
explain_bad_assumption env c
| ReferenceVariables id ->
@@ -463,38 +486,39 @@ let explain_type_error env err =
| ElimArity (ind, aritylst, c, pj, okinds) ->
explain_elim_arity env ind aritylst c pj okinds
| CaseNotInductive cj ->
- explain_case_not_inductive env cj
+ explain_case_not_inductive env sigma cj
| NumberBranches (cj, n) ->
- explain_number_branches env cj n
+ explain_number_branches env sigma cj n
| IllFormedBranch (c, i, actty, expty) ->
- explain_ill_formed_branch env c i actty expty
+ explain_ill_formed_branch env sigma c i actty expty
| Generalization (nvar, c) ->
explain_generalization env nvar c
| ActualType (j, pt) ->
- explain_actual_type env j pt
+ explain_actual_type env sigma j pt
| CantApplyBadType (t, rator, randl) ->
- explain_cant_apply_bad_type env t rator randl
+ explain_cant_apply_bad_type env sigma t rator randl
| CantApplyNonFunctional (rator, randl) ->
- explain_cant_apply_not_functional env rator randl
+ explain_cant_apply_not_functional env sigma rator randl
| IllFormedRecBody (err, lna, i, fixenv, vdefj) ->
explain_ill_formed_rec_body env err lna i fixenv vdefj
| IllTypedRecBody (i, lna, vdefj, vargs) ->
- explain_ill_typed_rec_body env i lna vdefj vargs
+ explain_ill_typed_rec_body env sigma i lna vdefj vargs
| WrongCaseInfo (ind,ci) ->
explain_wrong_case_info env ind ci
-let explain_pretype_error env err =
+let explain_pretype_error env sigma err =
+ let env = env_nf_evar sigma env in
let env = make_all_name_different env in
match err with
- | CantFindCaseType c -> explain_cant_find_case_type env c
- | OccurCheck (n,c) -> explain_occur_check env n c
- | NotClean (n,c,k) -> explain_not_clean env n c k
+ | CantFindCaseType c -> explain_cant_find_case_type env sigma c
+ | OccurCheck (n,c) -> explain_occur_check env sigma n c
+ | NotClean (n,c,k) -> explain_not_clean env sigma n c k
| UnsolvableImplicit (evi,k,exp) -> explain_unsolvable_implicit env evi k exp
| VarNotFound id -> explain_var_not_found env id
- | UnexpectedType (actual,expect) -> explain_unexpected_type env actual expect
- | NotProduct c -> explain_not_product env c
- | CannotUnify (m,n) -> explain_cannot_unify env m n
- | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env m n sn
+ | UnexpectedType (actual,expect) -> explain_unexpected_type env sigma actual expect
+ | NotProduct c -> explain_not_product env sigma c
+ | CannotUnify (m,n) -> explain_cannot_unify env sigma m n
+ | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env sigma m n sn
| CannotGeneralize ty -> explain_refiner_cannot_generalize env ty
| NoOccurrenceFound (c, id) -> explain_no_occurrence_found env c id
| CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n
@@ -502,6 +526,7 @@ let explain_pretype_error env err =
explain_cannot_find_well_typed_abstraction env p l
| AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n
| NonLinearUnification (m,c) -> explain_non_linear_unification env m c
+ | TypingError t -> explain_type_error env sigma t
(* Typeclass errors *)
@@ -809,7 +834,7 @@ let explain_reduction_tactic_error = function
| Tacred.InvalidAbstraction (env,c,(env',e)) ->
str "The abstracted term" ++ spc () ++ pr_lconstr_env_at_top env c ++
spc () ++ str "is not well typed." ++ fnl () ++
- explain_type_error env' e
+ explain_type_error env' Evd.empty e
let explain_ltac_call_trace (nrep,last,trace,loc) =
let calls =
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index dd8a7d663e..119765aec9 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -19,9 +19,9 @@ open Logic
(** This module provides functions to explain the type errors. *)
-val explain_type_error : env -> type_error -> std_ppcmds
+val explain_type_error : env -> Evd.evar_map -> type_error -> std_ppcmds
-val explain_pretype_error : env -> pretype_error -> std_ppcmds
+val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> std_ppcmds
val explain_inductive_error : inductive_error -> std_ppcmds
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fe676b3b1c..78235f458a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1064,8 +1064,8 @@ let vernac_check_may_eval redexp glopt rc =
try
Evarutil.check_evars env sigma sigma' c;
Typeops.typing env c
- with P.PretypeError (_,P.UnsolvableImplicit _)
- | Compat.Loc.Exc_located (_,P.PretypeError (_,P.UnsolvableImplicit _)) ->
+ with P.PretypeError (_,_,P.UnsolvableImplicit _)
+ | Compat.Loc.Exc_located (_,P.PretypeError (_,_,P.UnsolvableImplicit _)) ->
Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) in
match redexp with
| None ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 09:35:30 +0000