From 9c2bbdd58b6935ea980e72289777a20b85fe4fdb Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 19 Sep 2014 21:10:33 +0200 Subject: Fixes in Ltac pattern-matching on primitive projections and pretyping which was not contracting the eta-expanded forms in presence of coercions. --- pretyping/constrMatching.ml | 6 +++++- pretyping/pretyping.ml | 23 +++++++++++------------ 2 files changed, 16 insertions(+), 13 deletions(-) diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml index d4cbad054..7af639633 100644 --- a/pretyping/constrMatching.ml +++ b/pretyping/constrMatching.ml @@ -229,7 +229,11 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c = (match c1, kind_of_term c2 with | PRef (ConstRef r), Proj (pr,c) when not (eq_constant r pr) -> raise PatternMatchingFailure - (* eta-expanded version of projection against projection *) + | PProj (pr1,c1), Proj (pr,c) -> + if eq_constant pr1 pr then + try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c) arg1 arg2 + with Invalid_argument _ -> raise PatternMatchingFailure + else raise PatternMatchingFailure | _, Proj (pr,c) -> let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in sorec stk env subst p term diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 93d65197b..5c18297c0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -563,6 +563,16 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var with Not_found -> [] else [] in + let app_f = + match kind_of_term fj.uj_val with + | Const (p, u) when Environ.is_projection p env -> + let pb = Environ.lookup_projection p env in + let npars = pb.Declarations.proj_npars in + fun n -> + if n == npars + 1 then fun _ v -> mkProj (p, v) + else fun f v -> applist (f, [v]) + | _ -> fun _ f v -> applist (f, [v]) + in let rec apply_rec env n resj candargs = function | [] -> resj | c::rest -> @@ -581,7 +591,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var args, nf_evar !evdref (j_val hj) else [], j_val hj in - let value, typ = applist (j_val resj, [ujval]), subst1 ujval c2 in + let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in let j = { uj_val = value; uj_type = typ } in apply_rec env (n+1) j candargs rest @@ -604,17 +614,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env) evdref c in let t = Retyping.get_type_of env !evdref c in make_judge c (* use this for keeping evars: resj.uj_val *) t - else if isConst f then - let c,_ = destConst f in (* Internalize as primitive projection *) - if is_projection c env then - let pb = lookup_projection c env in - let npars = pb.Declarations.proj_npars and argslen = Array.length args in - if npars < argslen then - let proj = mkProj (c, args.(npars)) in - let args = Array.sub args (npars+1) (argslen - (npars + 1)) in - make_judge (mkApp (proj,args)) resj.uj_type - else resj - else resj else resj | _ -> resj in -- cgit v1.2.3