diff options
| author | Matthieu Sozeau | 2014-10-11 12:11:07 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-10-11 12:15:49 +0200 |
| commit | d4b3de96f524887013c0955bd5b90f0311f086e6 (patch) | |
| tree | ea87e31c9c4681911c9dede29de2d1b51a86deec /pretyping | |
| parent | d65496f09c4b68fa318783e53f9cd6d5c18e1eb7 (diff) | |
Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name
for the record binder of classes. This name is no longer generated
in the kernel but part of the declaration. Also cleanup the interface
to recognize primitive records based on an option type instead of a
dynamic check of the length of an array.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 3 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 5 |
4 files changed, 5 insertions, 7 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 32ac374a1e..f3f58d4371 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1307,7 +1307,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn let mk_case pb (ci,pred,c,brs) = let mib = lookup_mind (fst ci.ci_ind) pb.env in match mib.mind_record with - | Some (cs, pbs) when Array.length pbs > 0 -> + | Some (Some (_, cs, pbs)) -> Reduction.beta_appvect brs.(0) (Array.map (fun p -> mkProj (Projection.make p false, c)) cs) | _ -> mkCase (ci,pred,c,brs) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index fc726c2307..cdb38ecea3 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -798,8 +798,7 @@ and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1), and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with - | Some (projs, pbs) when Array.length projs > 0 - && mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> + | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> let pars = mib.Declarations.mind_nparams in (try let l1' = Stack.tail pars sk1 in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 24bf7cbc03..91072dce8c 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -334,7 +334,7 @@ let get_constructors env (ind,params) = let get_projections env (ind,params) = let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in match mib.mind_record with - | Some (projs, pbs) when Array.length projs > 0 -> Some projs + | Some (Some (id, projs, pbs)) -> Some projs | _ -> None (* substitution in a signature *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 370f3cee9c..2a6fd6fe7d 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -523,8 +523,7 @@ let is_eta_constructor_app env f l1 = | Construct (((_, i as ind), j), u) when i == 0 && j == 1 -> let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with - | Some (exp,projs) when Array.length projs > 0 - && mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> + | Some (Some (_, exp,projs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> Array.length projs == Array.length l1 - mib.Declarations.mind_nparams | _ -> false) | _ -> false @@ -534,7 +533,7 @@ let eta_constructor_app env f l1 term = | Construct (((_, i as ind), j), u) -> let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with - | Some (projs, _) -> + | Some (Some (_, projs, _)) -> let npars = mib.Declarations.mind_nparams in let pars, l1' = Array.chop npars l1 in let arg = Array.append pars [|term|] in |