diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 3 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 8 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 16 | ||||
| -rw-r--r-- | pretyping/nativenorm.ml | 7 | ||||
| -rw-r--r-- | pretyping/unification.ml | 10 |
5 files changed, 26 insertions, 18 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index fe49d64c7a..23a985dc3e 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -690,8 +690,7 @@ and detype_r d flags avoid env sigma t = let c' = try let pb = Environ.lookup_projection p (snd env) in - (** FIXME: handle mutual records *) - let ind = (pb.Declarations.proj_ind, 0) in + let ind = pb.Declarations.proj_ind in let bodies = Inductiveops.legacy_match_projection (snd env) ind in let body = bodies.(pb.Declarations.proj_arg) in let ty = Retyping.get_type_of (snd env) sigma c in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6d08f66c1b..a71ef65081 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -510,7 +510,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let tM = Stack.zip evd apprM in miller_pfenning on_left (fun () -> if not_only_app then (* Postpone the use of an heuristic *) - switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM + switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM else quick_fail i) ev lF tM i and consume (termF,skF as apprF) (termM,skM as apprM) i = @@ -578,7 +578,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty i,mkEvar ev else i,Stack.zip evd apprF in - switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) + switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) tF tR else UnifFailure (evd,OccurCheck (fst ev,tR)))]) @@ -984,9 +984,11 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) else UnifFailure(evd,(*dummy*)NotSameHead) and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = + let open Declarations in let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with - | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Declarations.BiFinite -> + | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite -> + let (_, projs, _) = info.(snd ind) in 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 1003f86c56..d599afe699 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -277,8 +277,8 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p let has_dependent_elim mib = match mib.mind_record with - | Some (Some _) -> mib.mind_finite == BiFinite - | _ -> true + | PrimRecord _ -> mib.mind_finite == BiFinite + | NotRecord | FakeRecord -> true (* Annotation for cases *) let make_case_info env ind style = @@ -346,8 +346,10 @@ 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 (Some (id, projs, pbs)) -> Some projs - | _ -> None + | PrimRecord infos -> + let (_, projs, _) = infos.(snd (fst ind)) in + Some projs + | NotRecord | FakeRecord -> None let make_case_or_project env sigma indf ci pred c branches = let open EConstr in @@ -460,7 +462,7 @@ let build_branch_type env sigma dep p cs = build an expansion function. The term built is expecting to be substituted first by a substitution of the form [params, x : ind params] *) -let compute_projections env (kn, _ as ind) = +let compute_projections env (kn, i as ind) = let open Term in let mib = Environ.lookup_mind kn env in let indu = match mib.mind_universes with @@ -470,9 +472,9 @@ let compute_projections env (kn, _ as ind) = mkIndU (ind, make_abstract_instance (ACumulativityInfo.univ_context ctx)) in let x = match mib.mind_record with - | None | Some None -> + | NotRecord | FakeRecord -> anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") - | Some (Some (id, _, _)) -> Name id + | PrimRecord info-> Name (pi1 (info.(i))) in (** FIXME: handle mutual records *) let pkt = mib.mind_packets.(0) in diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 4b8e0e0964..7319846fb3 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -188,12 +188,13 @@ let branch_of_switch lvl ans bs = bs ci in Array.init (Array.length tbl) branch -let get_proj env ((mind, _n), i) = +let get_proj env ((mind, n), i) = let mib = Environ.lookup_mind mind env in match mib.mind_record with - | None | Some None -> + | NotRecord | FakeRecord -> CErrors.anomaly (Pp.strbrk "Return type is not a primitive record") - | Some (Some (_, projs, _)) -> + | PrimRecord info -> + let _, projs, _ = info.(n) in Projection.make projs.(i) true let rec nf_val env sigma v typ = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5cf6e4b262..4ba5d27947 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -656,10 +656,12 @@ let rec is_neutral env sigma ts t = let is_eta_constructor_app env sigma ts f l1 term = match EConstr.kind sigma f with - | Construct (((_, i as ind), j), u) when i == 0 && j == 1 -> + | Construct (((_, i as ind), j), u) when j == 1 -> + let open Declarations in let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with - | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Declarations.BiFinite && + | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite && + let (_, projs, _) = info.(i) in Array.length projs == Array.length l1 - mib.Declarations.mind_nparams -> (** Check that the other term is neutral *) is_neutral env sigma ts term @@ -667,11 +669,13 @@ let is_eta_constructor_app env sigma ts f l1 term = | _ -> false let eta_constructor_app env sigma f l1 term = + let open Declarations in match EConstr.kind sigma f with | Construct (((_, i as ind), j), u) -> let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with - | Some (Some (_, projs, _)) -> + | PrimRecord info -> + let (_, projs, _) = info.(i) in let npars = mib.Declarations.mind_nparams in let pars, l1' = Array.chop npars l1 in let arg = Array.append pars [|term|] in |