aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml2
-rw-r--r--vernac/classes.ml2
-rw-r--r--vernac/comDefinition.ml91
-rw-r--r--vernac/comInductive.ml3
-rw-r--r--vernac/indschemes.ml6
-rw-r--r--vernac/lemmas.ml4
-rw-r--r--vernac/record.ml6
7 files changed, 57 insertions, 57 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 51dd5cd4f5..ec6b62ee27 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -317,7 +317,7 @@ let build_beq_scheme mode kn =
let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in
if not (Sorts.List.mem InSet kelim) then
raise (NonSingletonProp (kn,i));
- if mib.mind_finite = Decl_kinds.CoFinite then
+ if mib.mind_finite = CoFinite then
raise NoDecidabilityCoInductive;
let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in
create_input fix),
diff --git a/vernac/classes.ml b/vernac/classes.ml
index c2e9a5ab44..6914f899b7 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -141,7 +141,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
(fun avoid (clname, _) ->
match clname with
- | Some (cl, b) ->
+ | Some cl ->
let t = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) in
t, avoid
| None -> failwith ("new instance: under-applied typeclass"))
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 883121479f..d376696f76 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -11,7 +11,6 @@ open Util
open Constr
open Environ
open Entries
-open Termops
open Redexpr
open Declare
open Constrintern
@@ -49,55 +48,57 @@ let warn_implicits_in_term =
strbrk "Implicit arguments declaration relies on type." ++ spc () ++
strbrk "The term declares more implicits than the type here.")
+let check_imps ~impsty ~impsbody =
+ let b =
+ try
+ List.for_all (fun (key, (va:bool*bool*bool)) ->
+ (* Pervasives.(=) is OK for this type *)
+ Pervasives.(=) (List.assoc_f Impargs.explicitation_eq key impsty) va)
+ impsbody
+ with Not_found -> false
+ in
+ if not b then warn_implicits_in_term ()
+
let interp_definition pl bl poly red_option c ctypopt =
+ let open EConstr in
let env = Global.env() in
+ (* Explicitly bound universes and constraints *)
let evd, decl = Univdecls.interp_univ_decl_opt env pl in
+ (* Build the parameters *)
let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars env evd bl in
- let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in
- let nb_args = Context.Rel.nhyps ctx in
- let evd,imps,ce =
- match ctypopt with
- None ->
- let evd, subst = Evd.nf_univ_variables evd in
- let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
- let env_bl = push_rel_context ctx env in
- let evd, (c, imps2) = interp_constr_evars_impls ~impls env_bl evd c in
- let c = EConstr.Unsafe.to_constr c in
- let evd,nf = Evarutil.nf_evars_and_universes evd in
- let body = nf (it_mkLambda_or_LetIn c ctx) in
- let vars = EConstr.universes_of_constr env evd (EConstr.of_constr body) in
- let evd = Evd.restrict_universe_context evd vars in
- let uctx = Evd.check_univ_decl ~poly evd decl in
- evd, imps1@(Impargs.lift_implicits nb_args imps2),
- definition_entry ~univs:uctx body
- | Some ctyp ->
- let evd, (ty, impsty) = interp_type_evars_impls ~impls env_bl evd ctyp in
- let evd, subst = Evd.nf_univ_variables evd in
- let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
- let env_bl = push_rel_context ctx env in
- let evd, (c, imps2) = interp_casted_constr_evars_impls ~impls env_bl evd c ty in
- let c = EConstr.Unsafe.to_constr c in
- let evd, nf = Evarutil.nf_evars_and_universes evd in
- let body = nf (it_mkLambda_or_LetIn c ctx) in
- let ty = EConstr.Unsafe.to_constr ty in
- let typ = nf (Term.it_mkProd_or_LetIn ty ctx) in
- let beq b1 b2 = if b1 then b2 else not b2 in
- let impl_eq (x,y,z) (x',y',z') = beq x x' && beq y y' && beq z z' in
- (* Check that all implicit arguments inferable from the term
- are inferable from the type *)
- let chk (key,va) =
- impl_eq (List.assoc_f Pervasives.(=) key impsty) va (* FIXME *)
- in
- if not (try List.for_all chk imps2 with Not_found -> false)
- then warn_implicits_in_term ();
- let bodyvars = EConstr.universes_of_constr env evd (EConstr.of_constr body) in
- let tyvars = EConstr.universes_of_constr env evd (EConstr.of_constr ty) in
- let vars = Univ.LSet.union bodyvars tyvars in
- let evd = Evd.restrict_universe_context evd vars in
- let uctx = Evd.check_univ_decl ~poly evd decl in
- evd, imps1@(Impargs.lift_implicits nb_args impsty),
- definition_entry ~types:typ ~univs:uctx body
+ (* Build the type *)
+ let evd, tyopt = Option.fold_left_map
+ (interp_type_evars_impls ~impls env_bl)
+ evd ctypopt
+ in
+ (* Build the body, and merge implicits from parameters and from type/body *)
+ let evd, c, imps, tyopt =
+ match tyopt with
+ | None ->
+ let evd, (c, impsbody) = interp_constr_evars_impls ~impls env_bl evd c in
+ evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsbody, None
+ | Some (ty, impsty) ->
+ let evd, (c, impsbody) = interp_casted_constr_evars_impls ~impls env_bl evd c ty in
+ check_imps ~impsty ~impsbody;
+ evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty
+ in
+ (* universe minimization *)
+ let evd = Evd.nf_constraints evd in
+ (* Substitute evars and universes, and add parameters.
+ Note: in program mode some evars may remain. *)
+ let ctx = List.map (EConstr.to_rel_decl evd) ctx in
+ let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr evd c) ctx in
+ let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr evd ty) ctx) tyopt in
+ (* Keep only useful universes. *)
+ let uvars_fold uvars c =
+ Univ.LSet.union uvars (universes_of_constr env evd (of_constr c))
in
+ let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [c]) in
+ let evd = Evd.restrict_universe_context evd uvars in
+ (* Check we conform to declared universes *)
+ let uctx = Evd.check_univ_decl ~poly evd decl in
+ (* We're done! *)
+ let ce = definition_entry ?types:tyopt ~univs:uctx c in
(red_constant_entry (Context.Rel.length ctx) ce evd red_option, evd, decl, imps)
let check_definition (ce, evd, _, imps) =
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index f3f50f41dd..1c8677e9cd 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -25,7 +25,6 @@ open Nametab
open Impargs
open Reductionops
open Indtypes
-open Decl_kinds
open Pretyping
open Evarutil
open Indschemes
@@ -411,7 +410,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
(* spiwack: raises an error if the structure is supposed to be non-recursive,
but isn't *)
begin match mie.mind_entry_finite with
- | BiFinite when is_recursive mie ->
+ | Declarations.BiFinite when is_recursive mie ->
if Option.has_some mie.mind_entry_record then
user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.")
else
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index e4ca98749c..2f4c95affc 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -258,7 +258,7 @@ let declare_one_induction_scheme ind =
let declare_induction_schemes kn =
let mib = Global.lookup_mind kn in
- if mib.mind_finite <> Decl_kinds.CoFinite then begin
+ if mib.mind_finite <> Declarations.CoFinite then begin
for i = 0 to Array.length mib.mind_packets - 1 do
declare_one_induction_scheme (kn,i);
done;
@@ -268,7 +268,7 @@ let declare_induction_schemes kn =
let declare_eq_decidability_gen internal names kn =
let mib = Global.lookup_mind kn in
- if mib.mind_finite <> Decl_kinds.CoFinite then
+ if mib.mind_finite <> Declarations.CoFinite then
ignore (define_mutual_scheme eq_dec_scheme_kind internal names kn)
let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *)
@@ -512,7 +512,7 @@ let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done
let declare_default_schemes kn =
let mib = Global.lookup_mind kn in
let n = Array.length mib.mind_packets in
- if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag)
+ if !elim_flag && (mib.mind_finite <> Declarations.BiFinite || !bifinite_elim_flag)
&& mib.mind_typing_flags.check_guarded then
declare_induction_schemes kn;
if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n;
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 27a680b9b6..6ef310837c 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -100,7 +100,7 @@ let find_mutually_recursive_statements sigma thms =
match EConstr.kind sigma t with
| Ind ((kn,_ as ind),u) when
let mind = Global.lookup_mind kn in
- mind.mind_finite <> Decl_kinds.CoFinite ->
+ mind.mind_finite <> Declarations.CoFinite ->
[ind,x,i]
| _ ->
[]) 0 (List.rev (List.filter Context.Rel.Declaration.is_local_assum whnf_hyp_hds))) in
@@ -110,7 +110,7 @@ let find_mutually_recursive_statements sigma thms =
match EConstr.kind sigma whnf_ccl with
| Ind ((kn,_ as ind),u) when
let mind = Global.lookup_mind kn in
- Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite ->
+ Int.equal mind.mind_ntypes n && mind.mind_finite == Declarations.CoFinite ->
[ind,x,0]
| _ ->
[] in
diff --git a/vernac/record.ml b/vernac/record.ml
index 114b55cb40..d9dc16d96e 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -143,7 +143,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in
let assums = List.filter is_local_assum newps in
let params = List.map (RelDecl.get_name %> Name.get_id) assums in
- let ty = Inductive (params,(finite != BiFinite)) in
+ let ty = Inductive (params,(finite != Declarations.BiFinite)) in
let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr sigma arity] [imps] in
let env2,sigma,impls,newfs,data =
interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs)
@@ -507,7 +507,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
| Monomorphic_const_entry univs ->
Monomorphic_ind_entry univs
in
- let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls
+ let ind = declare_structure Declarations.BiFinite ubinders univs (snd id) idbuild paramimpls
params arity template fieldimpls fields
~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
in
@@ -523,7 +523,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
let ctx_context =
List.map (fun decl ->
match Typeclasses.class_of_constr Evd.empty (EConstr.of_constr (RelDecl.get_type decl)) with
- | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true)
+ | Some (_, ((cl,_), _)) -> Some cl.cl_impl
| None -> None)
params, params
in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 00:05:38 +0000