diff options
| author | Pierre-Marie Pédrot | 2018-07-24 17:58:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-24 17:58:01 +0200 |
| commit | 3599d05a5b3664764f19a794dc69c4e28f2e135d (patch) | |
| tree | ee65c9840649332663491ead6073f1323f4a6fb5 /pretyping/pretyping.ml | |
| parent | 388e65b550a6dd12fa4e59b26e03a831ebd842ce (diff) | |
| parent | 277563ab74a0529c330343479a063f808baa6db4 (diff) | |
Merge PR #7908: Projections use index representation
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 122979c1a0..3b9a8e6a1d 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -773,11 +773,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre in let app_f = match EConstr.kind !evdref fj.uj_val with - | Const (p, u) when Environ.is_projection p env.ExtraEnv.env -> + | Const (p, u) when Recordops.is_primitive_projection p -> + let p = Option.get @@ Recordops.find_primitive_projection p in let p = Projection.make p false in - let pb = Environ.lookup_projection p env.ExtraEnv.env in - let npars = pb.Declarations.proj_npars in - fun n -> + let npars = Projection.npars p 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]) @@ -905,6 +905,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let cloc = loc_of_glob_constr c in error_case_not_inductive ?loc:cloc env.ExtraEnv.env !evdref cj in + let ind = fst (fst (dest_ind_family indf)) in let cstrs = get_constructors env.ExtraEnv.env indf in if not (Int.equal (Array.length cstrs) 1) then user_err ?loc (str "Destructing let is only for inductive types" ++ @@ -915,7 +916,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre int cs.cs_nargs ++ str " variables."); let fsign, record = let set_name na d = set_name na (map_rel_decl EConstr.of_constr d) in - match get_projections env.ExtraEnv.env indf with + match Environ.get_projections env.ExtraEnv.env ind with | None -> List.map2 set_name (List.rev nal) cs.cs_args, false | Some ps -> |