diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/coercion.ml | 1 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 6 | ||||
| -rw-r--r-- | pretyping/pretype_errors.ml | 4 | ||||
| -rw-r--r-- | pretyping/pretype_errors.mli | 4 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 24 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 1 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 1 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 4 | ||||
| -rw-r--r-- | pretyping/tacred.mli | 4 |
9 files changed, 26 insertions, 23 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..dd38ec6f64 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -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..24767ca4d1 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) -> @@ -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/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] *) |