aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/coercion.ml1
-rw-r--r--pretyping/evarsolve.ml8
-rw-r--r--pretyping/pretype_errors.ml4
-rw-r--r--pretyping/pretype_errors.mli4
-rw-r--r--pretyping/pretyping.ml26
-rw-r--r--pretyping/reductionops.ml1
-rw-r--r--pretyping/reductionops.mli1
-rw-r--r--pretyping/retyping.ml8
-rw-r--r--pretyping/tacred.ml4
-rw-r--r--pretyping/tacred.mli4
10 files changed, 32 insertions, 29 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index e15c00f7dc..e21c2fda85 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -104,6 +104,7 @@ let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env ev
Evar_kinds.qm_name=na;
}) in
let evd, v = Evarutil.new_evar env !evdref ~src c in
+ let evd = Evd.set_obligation_evar evd (fst (destEvar evd v)) in
evdref := evd;
v
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 674f6846ae..96213af9c6 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -83,7 +83,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
(** Refresh the types of evars under template polymorphic references *)
let rec refresh_term_evars ~onevars ~top t =
match EConstr.kind !evdref t with
- | App (f, args) when is_template_polymorphic env !evdref f ->
+ | App (f, args) when Termops.is_template_polymorphic_ind env !evdref f ->
let pos = get_polymorphic_positions !evdref f in
refresh_polymorphic_positions args pos; t
| App (f, args) when top && isEvar !evdref f ->
@@ -1240,9 +1240,9 @@ let check_evar_instance evd evk1 body conv_algo =
let update_evar_info ev1 ev2 evd =
(* We update the source of obligation evars during evar-evar unifications. *)
- let loc, evs2 = evar_source ev2 evd in
- let evi = Evd.find evd ev1 in
- Evd.add evd ev1 {evi with evar_source = loc, evs2}
+ let loc, evs1 = evar_source ev1 evd in
+ let evi = Evd.find evd ev2 in
+ Evd.add evd ev2 {evi with evar_source = loc, evs1}
let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
try
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 856894d9a6..01b0d96f98 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -164,8 +164,8 @@ let error_not_product ?loc env sigma c =
(*s Error in conversion from AST to glob_constr *)
-let error_var_not_found ?loc s =
- raise_pretype_error ?loc (empty_env, Evd.from_env empty_env, VarNotFound s)
+let error_var_not_found ?loc env sigma s =
+ raise_pretype_error ?loc (env, sigma, VarNotFound s)
(*s Typeclass errors *)
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 6f14d025c7..054f0c76a9 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -150,9 +150,7 @@ val error_unexpected_type :
val error_not_product :
?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b
-(** {6 Error in conversion from AST to glob_constr } *)
-
-val error_var_not_found : ?loc:Loc.t -> Id.t -> 'b
+val error_var_not_found : ?loc:Loc.t -> env -> Evd.evar_map -> Id.t -> 'b
(** {6 Typeclass errors } *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 37afcf75e1..cba1533da5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -390,7 +390,7 @@ let pretype_id pretype k0 loc env sigma id =
sigma, { uj_val = mkVar id; uj_type = NamedDecl.get_type (lookup_named id !!env) }
with Not_found ->
(* [id] not found, standard error message *)
- error_var_not_found ?loc id
+ error_var_not_found ?loc !!env sigma id
(*************************************************************************)
(* Main pretyping function *)
@@ -436,7 +436,7 @@ let pretype_ref ?loc sigma env ref us =
(* This may happen if env is a goal env and section variables have
been cleared - section variables should be different from goal
variables *)
- Pretype_errors.error_var_not_found ?loc id)
+ Pretype_errors.error_var_not_found ?loc !!env sigma id)
| ref ->
let sigma, c = pretype_global ?loc univ_flexible env sigma ref us in
let ty = unsafe_type_of !!env sigma c in
@@ -457,6 +457,15 @@ let pretype_sort ?loc sigma = function
let new_type_evar env sigma loc =
new_type_evar env sigma ~src:(Loc.tag ?loc Evar_kinds.InternalHole)
+let mark_obligation_evar sigma k evc =
+ if Flags.is_program_mode () then
+ match k with
+ | Evar_kinds.QuestionMark _
+ | Evar_kinds.ImplicitArg (_, _, false) ->
+ Evd.set_obligation_evar sigma (fst (destEvar sigma evc))
+ | _ -> sigma
+ else sigma
+
(* [pretype tycon env sigma lvar lmeta cstr] attempts to type [cstr] *)
(* in environment [env], with existential variables [sigma] and *)
(* the type constraint tycon *)
@@ -510,15 +519,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
| Some ty -> sigma, ty
| None -> new_type_evar env sigma loc in
let sigma, uj_val = new_evar env sigma ~src:(loc,k) ~naming ty in
- let sigma =
- if Flags.is_program_mode () then
- match k with
- | Evar_kinds.QuestionMark _
- | Evar_kinds.ImplicitArg (_, _, false) ->
- Evd.set_obligation_evar sigma (fst (destEvar sigma uj_val))
- | _ -> sigma
- else sigma
- in
+ let sigma = mark_obligation_evar sigma k uj_val in
sigma, { uj_val; uj_type = ty }
| GHole (k, _naming, Some arg) ->
@@ -691,7 +692,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
let sigma, resj =
match EConstr.kind sigma resj.uj_val with
| App (f,args) ->
- if is_template_polymorphic !!env sigma f then
+ if Termops.is_template_polymorphic_ind !!env sigma f then
(* Special case for inductive type applications that must be
refreshed right away. *)
let c = mkApp (f, args) in
@@ -1039,6 +1040,7 @@ and pretype_type k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get
| None ->
let sigma, s = new_sort_variable univ_flexible_alg sigma in
let sigma, utj_val = new_evar env sigma ~src:(loc, knd) ~naming (mkSort s) in
+ let sigma = mark_obligation_evar sigma knd utj_val in
sigma, { utj_val; utj_type = s})
| _ ->
let sigma, j = pretype k0 resolve_tc empty_tycon env sigma c in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 367a48cb5e..aced97e910 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1251,6 +1251,7 @@ let clos_whd_flags flgs env sigma t =
let nf_beta = clos_norm_flags CClosure.beta
let nf_betaiota = clos_norm_flags CClosure.betaiota
let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta
+let nf_zeta = clos_norm_flags CClosure.zeta
let nf_all env sigma =
clos_norm_flags CClosure.all env sigma
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index c0ff6723f6..41de779414 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -171,6 +171,7 @@ val clos_whd_flags : CClosure.RedFlags.reds -> reduction_function
val nf_beta : reduction_function
val nf_betaiota : reduction_function
val nf_betaiotazeta : reduction_function
+val nf_zeta : reduction_function
val nf_all : reduction_function
val nf_evar : evar_map -> constr -> constr
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 7e43c5e41d..62ad296ecb 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -130,7 +130,7 @@ let retype ?(polyprop=true) sigma =
subst1 b (type_of (push_rel (LocalDef (name,b,c1)) env) c2)
| Fix ((_,i),(_,tys,_)) -> tys.(i)
| CoFix (i,(_,tys,_)) -> tys.(i)
- | App(f,args) when is_template_polymorphic env sigma f ->
+ | App(f,args) when Termops.is_template_polymorphic_ind env sigma f ->
let t = type_of_global_reference_knowing_parameters env f args in
strip_outer_cast sigma (subst_type env sigma t (Array.to_list args))
| App(f,args) ->
@@ -156,7 +156,7 @@ let retype ?(polyprop=true) sigma =
let dom = sort_of env t in
let rang = sort_of (push_rel (LocalAssum (name,t)) env) c2 in
Typeops.sort_of_product env dom rang
- | App(f,args) when is_template_polymorphic env sigma f ->
+ | App(f,args) when Termops.is_template_polymorphic_ind env sigma f ->
let t = type_of_global_reference_knowing_parameters env f args in
sort_of_atomic_type env sigma t args
| App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
@@ -190,14 +190,14 @@ let get_sort_family_of ?(truncation_style=false) ?(polyprop=true) env sigma t =
let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in
if not (is_impredicative_set env) &&
s2 == InSet && sort_family_of env t == InType then InType else s2
- | App(f,args) when is_template_polymorphic env sigma f ->
+ | App(f,args) when Termops.is_template_polymorphic_ind env sigma f ->
if truncation_style then InType else
let t = type_of_global_reference_knowing_parameters env f args in
Sorts.family (sort_of_atomic_type env sigma t args)
| App(f,args) ->
Sorts.family (sort_of_atomic_type env sigma (type_of env f) args)
| Lambda _ | Fix _ | Construct _ -> retype_error NotAType
- | Ind _ when truncation_style && is_template_polymorphic env sigma t -> InType
+ | Ind _ when truncation_style && Termops.is_template_polymorphic_ind env sigma t -> InType
| _ ->
Sorts.family (decomp_sort env sigma (type_of env t))
in sort_family_of env t
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 8911a2f343..4ec8569dd8 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1135,8 +1135,8 @@ let fold_commands cl env sigma c =
let cbv_norm_flags flags env sigma t =
cbv_norm (create_cbv_infos flags env sigma) t
-let cbv_beta = cbv_norm_flags beta empty_env
-let cbv_betaiota = cbv_norm_flags betaiota empty_env
+let cbv_beta = cbv_norm_flags beta
+let cbv_betaiota = cbv_norm_flags betaiota
let cbv_betadeltaiota env sigma = cbv_norm_flags all env sigma
let compute = cbv_betadeltaiota
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index bf38c30a1f..0887d0efd3 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -69,8 +69,8 @@ val pattern_occs : (occurrences * constr) list -> e_reduction_function
(** Call by value strategy (uses Closures) *)
val cbv_norm_flags : CClosure.RedFlags.reds -> reduction_function
- val cbv_beta : local_reduction_function
- val cbv_betaiota : local_reduction_function
+ val cbv_beta : reduction_function
+ val cbv_betaiota : reduction_function
val cbv_betadeltaiota : reduction_function
val compute : reduction_function (** = [cbv_betadeltaiota] *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 06:15:17 +0000