diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-02-20 12:40:35 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-02-20 12:40:35 +0000 |
commit | 18ea9b8400e03b815f81fcff3c79459d2b5db1f6 (patch) | |
tree | 8c6e95c724471aa7cc44803157b0150d08f4f0e1 | |
parent | 18e6108339aaf18499c1c64f05655f442ab100f8 (diff) |
Correct application of head reduction.
Fix a regression in subtac_pretyping, avoiding application of bidirectional application checking in
case the return type is a subset (bad interaction with typeclass overloading). Should be done only
on constructor applications.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14985 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | plugins/subtac/subtac_classes.ml | 6 | ||||
-rw-r--r-- | plugins/subtac/subtac_coercion.ml | 58 | ||||
-rw-r--r-- | plugins/subtac/subtac_pretyping_F.ml | 4 |
3 files changed, 38 insertions, 30 deletions
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index 4b53a2038..cac0988c0 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -107,9 +107,11 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in Namegen.next_global_ident_away i (Termops.ids_of_context env) in - let env' = push_rel_context ctx env in evars := Typeclasses.mark_resolvables (Evarutil.nf_evar_map !evars); evars := resolve_typeclasses ~onlyargs:false ~fail:true env !evars; + let ctx = Evarutil.nf_rel_context_evar !evars ctx + and ctx' = Evarutil.nf_rel_context_evar !evars ctx' in + let env' = push_rel_context ctx env in let sigma = !evars in let subst = List.map (Evarutil.nf_evar sigma) subst in let props = @@ -157,6 +159,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst) in evars := Evarutil.nf_evar_map !evars; + evars := Typeclasses.mark_resolvables !evars; + evars := resolve_typeclasses ~onlyargs:true ~fail:true env !evars; let term, termtype = match subst with | Inl subst -> diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml index 83555716d..eb29bd045 100644 --- a/plugins/subtac/subtac_coercion.ml +++ b/plugins/subtac/subtac_coercion.ml @@ -28,7 +28,7 @@ open Eterm open Pp let app_opt env evars f t = - Tacred.simpl env !evars (app_opt f t) + whd_betaiota !evars (app_opt f t) let pair_of_array a = (a.(0), a.(1)) let make_name s = Name (id_of_string s) @@ -83,7 +83,8 @@ module Coercion = struct | Type _, Prop Null -> Prop Null | _, Type _ -> s2 - let hnf env isevars c = whd_betadeltaiota env ( !isevars) c + let hnf env isevars c = whd_betadeltaiota env isevars c + let hnf_nodelta env evars c = whd_betaiota evars c let lift_args n sign = let rec liftrec k = function @@ -94,15 +95,15 @@ module Coercion = struct let rec mu env isevars t = let rec aux v = - let v = hnf env isevars v in + let v = hnf env !isevars v in match disc_subset v with Some (u, p) -> let f, ct = aux u in - let p = hnf env isevars p in + let p = hnf env !isevars p in (Some (fun x -> - app_opt env isevars - f (mkApp ((delayed_force sig_).proj1, - [| u; p; x |]))), + app_opt env isevars + f (mkApp ((delayed_force sig_).proj1, + [| u; p; x |]))), ct) | None -> (None, v) in aux t @@ -111,7 +112,7 @@ module Coercion = struct : (Term.constr -> Term.constr) option = let rec coerce_unify env x y = - let x = hnf env isevars x and y = hnf env isevars y in + let x = hnf env !isevars x and y = hnf env !isevars y in try isevars := the_conv_x_leq env x y !isevars; None @@ -359,7 +360,7 @@ module Coercion = struct let inh_app_fun env isevars j = let isevars = ref isevars in - let t = whd_betadeltaiota env !isevars j.uj_type in + let t = hnf env !isevars j.uj_type in match kind_of_term t with | Prod (_,_,_) -> (!isevars,j) | Evar ev when not (is_defined_evar !isevars ev) -> @@ -387,7 +388,7 @@ module Coercion = struct error_not_a_type_loc loc env ( isevars) j let inh_coerce_to_sort loc env isevars j = - let typ = whd_betadeltaiota env ( isevars) j.uj_type in + let typ = hnf env isevars j.uj_type in match kind_of_term typ with | Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s }) | Evar ev when not (is_defined_evar isevars ev) -> @@ -398,7 +399,7 @@ module Coercion = struct let inh_coerce_to_base loc env isevars j = let isevars = ref isevars in - let typ = whd_betadeltaiota env !isevars j.uj_type in + let typ = hnf env !isevars j.uj_type in let ct, typ' = mu env isevars typ in let res = { uj_val = app_opt env isevars ct j.uj_val; @@ -407,7 +408,7 @@ module Coercion = struct let inh_coerce_to_prod loc env isevars t = let isevars = ref isevars in - let typ = whd_betadeltaiota env !isevars (snd t) in + let typ = hnf env !isevars (snd t) in let _, typ' = mu env isevars typ in !isevars, (fst t, typ') @@ -462,22 +463,23 @@ module Coercion = struct (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) let inh_conv_coerce_to_gen rigidonly loc env evd cj ((n, t) as _tycon) = match n with - None -> - let (evd', val') = - try - inh_conv_coerce_to_fail loc env evd rigidonly - (Some cj.uj_val) cj.uj_type t - with NoCoercion -> - let sigma = evd in - try - coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t - with NoSubtacCoercion -> - error_actual_type_loc loc env sigma cj t - in - let val' = match val' with Some v -> v | None -> assert(false) in - (evd',{ uj_val = val'; uj_type = t }) - | Some (init, cur) -> - (evd, cj) + | None -> + let cj = { cj with uj_type = hnf_nodelta env evd cj.uj_type } + and t = hnf_nodelta env evd t in + let (evd', val') = + try + inh_conv_coerce_to_fail loc env evd rigidonly + (Some cj.uj_val) cj.uj_type t + with NoCoercion -> + (try + coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t + with NoSubtacCoercion -> + error_actual_type_loc loc env evd cj t) + in + let val' = match val' with Some v -> v | None -> assert(false) in + (evd',{ uj_val = val'; uj_type = t }) + | Some (init, cur) -> + (evd, cj) let inh_conv_coerce_to = inh_conv_coerce_to_gen false let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index ca5145d73..528a2e683 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -323,7 +323,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct else tycon in match ty with - | Some (_, t) when Subtac_coercion.disc_subset t = None -> ty + | Some (_, t) -> + if Subtac_coercion.disc_subset (whd_betadeltaiota env !evdref t) = None then ty + else None | _ -> None in let fj = pretype ftycon env evdref lvar f in |