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.ml8
-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
-rw-r--r--vernac/vernacentries.ml19
-rw-r--r--vernac/vernacprop.ml17
-rw-r--r--vernac/vernacprop.mli2
10 files changed, 73 insertions, 85 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..4a2dba859f 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -69,8 +69,7 @@ let existing_instance glob g info =
let instance, _ = Global.type_of_global_in_context (Global.env ()) c in
let _, r = Term.decompose_prod_assum instance in
match class_of_constr Evd.empty (EConstr.of_constr r) with
- | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob
- (*FIXME*) (Flags.use_polymorphic_flag ()) c)
+ | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob c)
| None -> user_err ?loc:(loc_of_reference g)
~hdr:"declare_instance"
(Pp.str "Constant does not build instances of a declared type class.")
@@ -141,7 +140,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"))
@@ -393,8 +392,7 @@ let context poly l =
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
match class_of_constr sigma (of_constr t) with
| Some (rels, ((tc,_), args) as _cl) ->
- add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (*FIXME*)
- poly (ConstRef cst));
+ add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (ConstRef cst));
status
(* declare_subclasses (ConstRef cst) cl *)
| None -> status
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
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index aa6121c39a..ded0d97e64 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2132,10 +2132,6 @@ let check_vernac_supports_polymorphism c p =
| VernacExtend _ | VernacUniverse _ | VernacConstraint _) -> ()
| Some _, _ -> user_err Pp.(str "This command does not support Polymorphism")
-let enforce_polymorphism = function
- | None -> Flags.is_universe_polymorphism ()
- | Some b -> Flags.make_polymorphic_flag b; b
-
(** A global default timeout, controlled by option "Set Default Timeout n".
Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
@@ -2202,6 +2198,7 @@ let with_fail st b f =
end
let interp ?(verbosely=true) ?proof ~st (loc,c) =
+ let orig_univ_poly = Flags.is_universe_polymorphism () in
let orig_program_mode = Flags.is_program_mode () in
let rec control = function
| VernacExpr v ->
@@ -2213,8 +2210,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
control v
| VernacRedirect (s, (_,v)) ->
Topfmt.with_output_to_file s control v
- | VernacTime (_,v) ->
- System.with_time !Flags.time control v;
+ | VernacTime (batch, (_loc,v)) ->
+ System.with_time ~batch control v;
and aux ?polymorphism ~atts isprogcmd = function
@@ -2241,7 +2238,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
| c ->
check_vernac_supports_locality c atts.locality;
check_vernac_supports_polymorphism c polymorphism;
- let polymorphic = enforce_polymorphism polymorphism in
+ let polymorphic = Option.default (Flags.is_universe_polymorphism ()) polymorphism in
+ Flags.make_universe_polymorphism polymorphic;
Obligations.set_program_mode isprogcmd;
try
vernac_timeout begin fun () ->
@@ -2249,9 +2247,12 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
if verbosely
then Flags.verbosely (interp ?proof ~atts ~st) c
else Flags.silently (interp ?proof ~atts ~st) c;
+ (* If the command is `(Un)Set Program Mode` or `(Un)Set Universe Polymorphism`,
+ we should not restore the previous state of the flag... *)
if orig_program_mode || not !Flags.program_mode || isprogcmd then
Flags.program_mode := orig_program_mode;
- ignore (Flags.use_polymorphic_flag ())
+ if (Flags.is_universe_polymorphism() = polymorphic) then
+ Flags.make_universe_polymorphism orig_univ_poly;
end
with
| reraise when
@@ -2262,8 +2263,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
let e = CErrors.push reraise in
let e = locate_if_not_already ?loc e in
let () = restore_timeout () in
+ Flags.make_universe_polymorphism orig_univ_poly;
Flags.program_mode := orig_program_mode;
- ignore (Flags.use_polymorphic_flag ());
iraise e
in
if verbosely
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 4a01ef2efa..4fdc78dd2a 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -14,14 +14,14 @@ open Vernacexpr
let rec under_control = function
| VernacExpr c -> c
| VernacRedirect (_,(_,c))
- | VernacTime (_,c)
+ | VernacTime (_,(_,c))
| VernacFail c
| VernacTimeout (_,c) -> under_control c
let rec has_Fail = function
| VernacExpr c -> false
| VernacRedirect (_,(_,c))
- | VernacTime (_,c)
+ | VernacTime (_,(_,c))
| VernacTimeout (_,c) -> has_Fail c
| VernacFail _ -> true
@@ -38,7 +38,7 @@ let is_navigation_vernac c =
is_navigation_vernac_expr (under_control c)
let rec is_deep_navigation_vernac = function
- | VernacTime (_,c) -> is_deep_navigation_vernac c
+ | VernacTime (_,(_,c)) -> is_deep_navigation_vernac c
| VernacRedirect (_, (_,c))
| VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
| VernacExpr _ -> false
@@ -53,17 +53,6 @@ let is_debug cmd = match under_control cmd with
| VernacSetOption (["Ltac";"Debug"], _) -> true
| _ -> false
-let is_query cmd = match under_control cmd with
- | VernacChdir None
- | VernacMemOption _
- | VernacPrintOption _
- | VernacCheckMayEval _
- | VernacGlobalCheck _
- | VernacPrint _
- | VernacSearch _
- | VernacLocate _ -> true
- | _ -> false
-
let is_undo cmd = match under_control cmd with
| VernacUndo _ | VernacUndoTo _ -> true
| _ -> false
diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli
index eb7c7055ac..df739f96a9 100644
--- a/vernac/vernacprop.mli
+++ b/vernac/vernacprop.mli
@@ -21,6 +21,6 @@ val has_Fail : vernac_control -> bool
val is_navigation_vernac : vernac_control -> bool
val is_deep_navigation_vernac : vernac_control -> bool
val is_reset : vernac_control -> bool
-val is_query : vernac_control -> bool
val is_debug : vernac_control -> bool
val is_undo : vernac_control -> bool
+
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 14:36:03 +0000