diff options
| -rw-r--r-- | pretyping/evarconv.ml | 4 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 13 | ||||
| -rw-r--r-- | pretyping/recordops.mli | 2 |
3 files changed, 12 insertions, 7 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 9b002a5bc..0f1a508c8 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -178,7 +178,9 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = (proji, Sort_cs (family_of_sort s)),[] | Proj (p, c) -> let c2 = Globnames.ConstRef (Projection.constant p) in - let sk2 = Stack.append_app [|c|] sk2 in + let c = Retyping.expand_projection env sigma p c [] in + let _, args = destApp sigma c in + let sk2 = Stack.append_app args sk2 in lookup_canonical_conversion (proji, Const_cs c2), sk2 | _ -> let (c2, _) = Termops.global_of_constr sigma t2 in diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 469b32eba..26b16c039 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -171,7 +171,7 @@ let keep_true_projections projs kinds = let filter (p, (_, b)) = if b then Some p else None in List.map_filter filter (List.combine projs kinds) -let cs_pattern_of_constr t = +let cs_pattern_of_constr env t = match kind_of_term t with App (f,vargs) -> begin @@ -181,7 +181,9 @@ let cs_pattern_of_constr t = | Rel n -> Default_cs, Some n, [] | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b] | Proj (p, c) -> - Const_cs (ConstRef (Projection.constant p)), None, [c] + let { Environ.uj_type = ty } = Typeops.infer env c in + let _, params = Inductive.find_rectype env ty in + Const_cs (ConstRef (Projection.constant p)), None, params @ [c] | Sort s -> Sort_cs (family_of_sort s), None, [] | _ -> begin @@ -192,7 +194,6 @@ let cs_pattern_of_constr t = let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" (fun (sign,env,t,con,proji_sp) -> - let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in let env = Termops.push_rels_assum sign env in let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in @@ -209,14 +210,16 @@ let compute_canonical_projections warn (con,ind) = let v = (mkConstU (con,u)) in let c = Environ.constant_value_in env (con,u) in let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in + let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in let t = EConstr.Unsafe.to_constr t in - let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) sign in + let lt = List.rev_map snd sign in let args = snd (decompose_app t) in let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in let params, projs = List.chop p args in let lpj = keep_true_projections lpj kl in let lps = List.combine lpj projs in + let nenv = Termops.push_rels_assum sign env in let comp = List.fold_left (fun l (spopt,t) -> (* comp=components *) @@ -224,7 +227,7 @@ let compute_canonical_projections warn (con,ind) = | Some proji_sp -> begin try - let patt, n , args = cs_pattern_of_constr t in + let patt, n , args = cs_pattern_of_constr nenv t in ((ConstRef proji_sp, patt, t, n, args) :: l) with Not_found -> if warn then warn_projection_no_head_constant (sign,env,t,con,proji_sp); diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 5480b14af..8e2333b34 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -65,7 +65,7 @@ type obj_typ = { o_TCOMPS : constr list } (** ordered *) (** Return the form of the component of a canonical structure *) -val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list +val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * constr list val pr_cs_pattern : cs_pattern -> Pp.t |