aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/attributes.ml44
-rw-r--r--vernac/attributes.mli3
-rw-r--r--vernac/comArguments.ml4
-rw-r--r--vernac/comDefinition.ml10
-rw-r--r--vernac/comDefinition.mli2
-rw-r--r--vernac/comFixpoint.ml33
-rw-r--r--vernac/comFixpoint.mli23
-rw-r--r--vernac/comInductive.ml8
-rw-r--r--vernac/comInductive.mli1
-rw-r--r--vernac/comProgramFixpoint.ml27
-rw-r--r--vernac/comProgramFixpoint.mli1
-rw-r--r--vernac/declare.ml64
-rw-r--r--vernac/declare.mli2
-rw-r--r--vernac/declareInd.ml8
-rw-r--r--vernac/declareInd.mli1
-rw-r--r--vernac/declareUniv.ml5
-rw-r--r--vernac/declareUniv.mli2
-rw-r--r--vernac/himsg.ml13
-rw-r--r--vernac/ppvernac.ml4
-rw-r--r--vernac/prettyp.ml4
-rw-r--r--vernac/vernacentries.ml81
-rw-r--r--vernac/vernacexpr.ml8
22 files changed, 228 insertions, 120 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index fdaeedef8c..37895d22f5 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -338,3 +338,47 @@ let uses_parser : string key_parser = fun orig args ->
| _ -> CErrors.user_err (Pp.str "Ill formed \"using\" attribute")
let using = attribute_of_list ["using",uses_parser]
+
+let process_typing_att ~typing_flags att disable =
+ let enable = not disable in
+ match att with
+ | "universes" ->
+ { typing_flags with
+ Declarations.check_universes = enable
+ }
+ | "guard" ->
+ { typing_flags with
+ Declarations.check_guarded = enable
+ }
+ | "positivity" ->
+ { typing_flags with
+ Declarations.check_positive = enable
+ }
+ | att ->
+ CErrors.user_err Pp.(str "Unknown “typing” attribute: " ++ str att)
+
+let process_typing_disable ~key = function
+ | VernacFlagEmpty | VernacFlagLeaf (FlagIdent "yes") ->
+ true
+ | VernacFlagLeaf (FlagIdent "no") ->
+ false
+ | _ ->
+ CErrors.user_err Pp.(str "Ill-formed attribute value, must be " ++ str key ++ str "={yes, no}")
+
+let typing_flags_parser : Declarations.typing_flags key_parser = fun orig args ->
+ let rec flag_parser typing_flags = function
+ | [] -> typing_flags
+ | (typing_att, enable) :: rest ->
+ let disable = process_typing_disable ~key:typing_att enable in
+ let typing_flags = process_typing_att ~typing_flags typing_att disable in
+ flag_parser typing_flags rest
+ in
+ match args with
+ | VernacFlagList atts ->
+ let typing_flags = Global.typing_flags () in
+ flag_parser typing_flags atts
+ | att ->
+ CErrors.user_err Pp.(str "Ill-formed “typing” attribute: " ++ pr_vernac_flag_value att)
+
+let typing_flags =
+ attribute_of_list ["bypass_check", typing_flags_parser]
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 03a14a03ff..584e13e781 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -59,6 +59,9 @@ val canonical_field : bool attribute
val canonical_instance : bool attribute
val using : string option attribute
+(** Enable/Disable universe checking *)
+val typing_flags : Declarations.typing_flags option attribute
+
val program_mode_option_name : string list
(** For internal use when messing with the global option. *)
diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml
index adf1f42beb..a21af12785 100644
--- a/vernac/comArguments.ml
+++ b/vernac/comArguments.ml
@@ -223,10 +223,10 @@ let vernac_arguments ~section_local reference args more_implicits flags =
| _ -> true in
if implicits_specified && clear_implicits_flag then
- CErrors.user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations");
+ CErrors.user_err Pp.(str "The \"clear implicits\" flag must be omitted if implicit annotations are given.");
if implicits_specified && default_implicits_flag then
- CErrors.user_err Pp.(str "The \"default implicits\" flag is incompatible with implicit annotations");
+ CErrors.user_err Pp.(str "The \"default implicits\" flag is incompatible with implicit annotations.");
let rargs =
Util.List.map_filter (function (n, true) -> Some n | _ -> None)
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 81154bbea9..c54adb45f9 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -110,9 +110,10 @@ let interp_definition ~program_mode env evd impl_env bl red_option c ctypopt =
let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in
evd, (c, tyopt), imps
-let do_definition ?hook ~name ~scope ~poly ~kind ?using udecl bl red_option c ctypopt =
+let do_definition ?hook ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl red_option c ctypopt =
let program_mode = false in
let env = Global.env() in
+ let env = Environ.update_typing_flags ?typing_flags env in
(* Explicitly bound universes and constraints *)
let evd, udecl = interp_univ_decl_opt env udecl in
let evd, (body, types), impargs =
@@ -125,14 +126,15 @@ let do_definition ?hook ~name ~scope ~poly ~kind ?using udecl bl red_option c ct
in
let kind = Decls.IsDefinition kind in
let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ?using () in
- let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly () in
+ let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly ?typing_flags () in
let _ : Names.GlobRef.t =
Declare.declare_definition ~info ~cinfo ~opaque:false ~body evd
in ()
-let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind ?using udecl bl red_option c ctypopt =
+let do_definition_program ?hook ~pm ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl red_option c ctypopt =
let program_mode = true in
let env = Global.env() in
+ let env = Environ.update_typing_flags ?typing_flags env in
(* Explicitly bound universes and constraints *)
let evd, udecl = interp_univ_decl_opt env udecl in
let evd, (body, types), impargs =
@@ -146,6 +148,6 @@ let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind ?using udecl bl red
let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in
let pm, _ =
let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in
- let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook () in
+ let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook ?typing_flags () in
Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls
in pm
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 5e1b705ae4..9962e44098 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -30,6 +30,7 @@ val do_definition
-> name:Id.t
-> scope:Locality.locality
-> poly:bool
+ -> ?typing_flags:Declarations.typing_flags
-> kind:Decls.definition_object_kind
-> ?using:Vernacexpr.section_subset_expr
-> universe_decl_expr option
@@ -45,6 +46,7 @@ val do_definition_program
-> name:Id.t
-> scope:Locality.locality
-> poly:bool
+ -> ?typing_flags:Declarations.typing_flags
-> kind:Decls.logical_kind
-> ?using:Vernacexpr.section_subset_expr
-> universe_decl_expr option
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index dd6c985bf9..0cf0b07822 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -158,10 +158,9 @@ type ('constr, 'types) recursive_preentry =
let fix_proto sigma =
Evarutil.new_global sigma (Coqlib.lib_ref "program.tactic.fix_proto")
-let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen list) =
+let interp_recursive env ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen list) =
let open Context.Named.Declaration in
let open EConstr in
- let env = Global.env() in
let fixnames = List.map (fun fix -> fix.Vernacexpr.fname.CAst.v) fixl in
(* Interp arities allowing for unresolved types *)
@@ -241,11 +240,13 @@ let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) =
Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes)
(* XXX: Unify with interp_recursive *)
-let interp_fixpoint ?(check_recursivity=true) ~cofix l :
+let interp_fixpoint ?(check_recursivity=true) ?typing_flags ~cofix l :
( (Constr.t, Constr.types) recursive_preentry *
UState.universe_decl * UState.t *
(EConstr.rel_context * Impargs.manual_implicits * int option) list) =
- let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l in
+ let env = Global.env () in
+ let env = Environ.update_typing_flags ?typing_flags env in
+ let (env,_,pl,evd),fix,info = interp_recursive env ~program_mode:false ~cofix l in
if check_recursivity then check_recursive true env evd fix;
let evd = Pretyping.(solve_remaining_evars all_no_fail_flags env evd) in
let uctx,fix = ground_fixpoint env evd fix in
@@ -271,12 +272,12 @@ let build_recthms ~indexes ?using fixnames fixtypes fiximps =
in
fix_kind, cofix, thms
-let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns =
+let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ?typing_flags ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns =
let fix_kind, cofix, thms = build_recthms ~indexes fixnames fixtypes fiximps in
let indexes = Option.default [] indexes in
let init_terms = Some fixdefs in
let evd = Evd.from_ctx ctx in
- let info = Declare.Info.make ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl () in
+ let info = Declare.Info.make ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl ?typing_flags () in
let lemma =
Declare.Proof.start_mutual_with_initialization ~info
evd ~mutual_info:(cofix,indexes,init_terms) ~cinfo:thms None in
@@ -284,13 +285,13 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
lemma
-let declare_fixpoint_generic ?indexes ~scope ~poly ?using ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
+let declare_fixpoint_generic ?indexes ~scope ~poly ?typing_flags ?using ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
(* We shortcut the proof process *)
let fix_kind, cofix, fixitems = build_recthms ~indexes ?using fixnames fixtypes fiximps in
let fixdefs = List.map Option.get fixdefs in
let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
let fix_kind = Decls.IsDefinition fix_kind in
- let info = Declare.Info.make ~scope ~kind:fix_kind ~poly ~udecl () in
+ let info = Declare.Info.make ~scope ~kind:fix_kind ~poly ~udecl ?typing_flags () in
let cinfo = fixitems in
let _ : GlobRef.t list =
Declare.declare_mutually_recursive ~cinfo ~info ~opaque:false ~uctx
@@ -322,22 +323,22 @@ let adjust_rec_order ~structonly binders rec_order =
in
Option.map (extract_decreasing_argument ~structonly) rec_order
-let do_fixpoint_common (fixl : Vernacexpr.fixpoint_expr list) =
+let do_fixpoint_common ?typing_flags (fixl : Vernacexpr.fixpoint_expr list) =
let fixl = List.map (fun fix ->
Vernacexpr.{ fix
with rec_order = adjust_rec_order ~structonly:true fix.binders fix.rec_order }) fixl in
let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in
- let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl in
+ let (_, _, _, info as fix) = interp_fixpoint ~cofix:false ?typing_flags fixl in
fixl, ntns, fix, List.map compute_possible_guardness_evidences info
-let do_fixpoint_interactive ~scope ~poly l : Declare.Proof.t =
- let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
- let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly fix ntns in
+let do_fixpoint_interactive ~scope ~poly ?typing_flags l : Declare.Proof.t =
+ let fixl, ntns, fix, possible_indexes = do_fixpoint_common ?typing_flags l in
+ let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly ?typing_flags fix ntns in
lemma
-let do_fixpoint ~scope ~poly ?using l =
- let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
- declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly ?using fix ntns
+let do_fixpoint ~scope ~poly ?typing_flags ?using l =
+ let fixl, ntns, fix, possible_indexes = do_fixpoint_common ?typing_flags l in
+ declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly ?typing_flags ?using fix ntns
let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) =
let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index a36aba7672..faa5fce375 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -15,11 +15,20 @@ open Vernacexpr
(** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
-val do_fixpoint_interactive :
- scope:Locality.locality -> poly:bool -> fixpoint_expr list -> Declare.Proof.t
+val do_fixpoint_interactive
+ : scope:Locality.locality
+ -> poly:bool
+ -> ?typing_flags:Declarations.typing_flags
+ -> fixpoint_expr list
+ -> Declare.Proof.t
-val do_fixpoint :
- scope:Locality.locality -> poly:bool -> ?using:Vernacexpr.section_subset_expr -> fixpoint_expr list -> unit
+val do_fixpoint
+ : scope:Locality.locality
+ -> poly:bool
+ -> ?typing_flags:Declarations.typing_flags
+ -> ?using:Vernacexpr.section_subset_expr
+ -> fixpoint_expr list
+ -> unit
val do_cofixpoint_interactive :
scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> Declare.Proof.t
@@ -44,6 +53,7 @@ type ('constr, 'types) recursive_preentry = Id.t list * Sorts.relevance list * '
(** Exported for Program *)
val interp_recursive :
+ Environ.env ->
(* Misc arguments *)
program_mode:bool -> cofix:bool ->
(* Notations of the fixpoint / should that be folded in the previous argument? *)
@@ -58,8 +68,9 @@ val interp_recursive :
(** Exported for Funind *)
val interp_fixpoint
- : ?check_recursivity:bool ->
- cofix:bool
+ : ?check_recursivity:bool
+ -> ?typing_flags:Declarations.typing_flags
+ -> cofix:bool
-> lident option fix_expr_gen list
-> (Constr.t, Constr.types) recursive_preentry *
UState.universe_decl * UState.t *
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 8cb077ca21..2be6097184 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -631,7 +631,7 @@ type uniform_inductive_flag =
| UniformParameters
| NonUniformParameters
-let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uniform finite =
+let do_mutual_inductive ~template udecl indl ~cumulative ~poly ?typing_flags ~private_ind ~uniform finite =
let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in
(* Interpret the types *)
let indl = match params with
@@ -640,9 +640,11 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni
| UniformParameters -> (params, [], indl)
| NonUniformParameters -> ([], params, indl)
in
- let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in
+ let env = Global.env () in
+ let env = Environ.update_typing_flags ?typing_flags env in
+ let mie,pl,impls = interp_mutual_inductive_gen env ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in
(* Declare the mutual inductive block with its associated schemes *)
- ignore (DeclareInd.declare_mutual_inductive_with_eliminations mie pl impls);
+ ignore (DeclareInd.declare_mutual_inductive_with_eliminations ?typing_flags mie pl impls);
(* Declare the possible notations of inductive types *)
List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns;
(* Declare the coercions *)
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 8bce884ba4..e049bacb26 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -26,6 +26,7 @@ val do_mutual_inductive
-> (one_inductive_expr * decl_notation list) list
-> cumulative:bool
-> poly:bool
+ -> ?typing_flags:Declarations.typing_flags
-> private_ind:bool
-> uniform:uniform_inductive_flag
-> Declarations.recursivity_kind
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 31f91979d3..3c4a651cf5 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -109,7 +109,7 @@ let telescope env sigma l =
let nf_evar_context sigma ctx =
List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx
-let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?using r measure notation =
+let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?typing_flags ?using r measure notation =
let open EConstr in
let open Vars in
let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
@@ -266,7 +266,7 @@ let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?using r measure notat
in
let uctx = Evd.evar_universe_context sigma in
let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ ?using () in
- let info = Declare.Info.make ~udecl ~poly ~hook () in
+ let info = Declare.Info.make ~udecl ~poly ~hook ?typing_flags () in
let pm, _ =
Declare.Obls.add_definition ~pm ~cinfo ~info ~term:evars_def ~uctx evars in
pm
@@ -280,10 +280,12 @@ let collect_evars_of_term evd c ty =
Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
evars (Evd.from_ctx (Evd.evar_universe_context evd))
-let do_program_recursive ~pm ~scope ~poly ?using fixkind fixl =
+let do_program_recursive ~pm ~scope ~poly ?typing_flags ?using fixkind fixl =
let cofix = fixkind = Declare.Obls.IsCoFixpoint in
let (env, rec_sign, udecl, evd), fix, info =
- interp_recursive ~cofix ~program_mode:true fixl
+ let env = Global.env () in
+ let env = Environ.update_typing_flags ?typing_flags env in
+ interp_recursive env ~cofix ~program_mode:true fixl
in
(* Program-specific code *)
(* Get the interesting evars, those that were not instantiated *)
@@ -320,10 +322,13 @@ let do_program_recursive ~pm ~scope ~poly ?using fixkind fixl =
Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
in
let indexes =
- Pretyping.search_guard (Global.env ()) possible_indexes fixdecls in
+ let env = Global.env () in
+ let env = Environ.update_typing_flags ?typing_flags env in
+ Pretyping.search_guard env possible_indexes fixdecls in
+ let env = Environ.update_typing_flags ?typing_flags env in
List.iteri (fun i _ ->
Inductive.check_fix env
- ((indexes,i),fixdecls))
+ ((indexes,i),fixdecls))
fixl
end in
let uctx = Evd.evar_universe_context evd in
@@ -332,16 +337,16 @@ let do_program_recursive ~pm ~scope ~poly ?using fixkind fixl =
| Declare.Obls.IsCoFixpoint -> Decls.(IsDefinition CoFixpoint)
in
let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in
- let info = Declare.Info.make ~poly ~scope ~kind ~udecl () in
+ let info = Declare.Info.make ~poly ~scope ~kind ~udecl ?typing_flags () in
Declare.Obls.add_mutual_definitions ~pm defs ~info ~uctx ~ntns fixkind
-let do_fixpoint ~pm ~scope ~poly ?using l =
+let do_fixpoint ~pm ~scope ~poly ?typing_flags ?using l =
let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
match g, l with
| [Some { CAst.v = CWfRec (n,r) }],
[ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] ->
let recarg = mkIdentC n.CAst.v in
- build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?using r recarg notations
+ build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?typing_flags ?using r recarg notations
| [Some { CAst.v = CMeasureRec (n, m, r) }],
[Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations }] ->
@@ -354,7 +359,7 @@ let do_fixpoint ~pm ~scope ~poly ?using l =
user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.")
| _, _ -> r
in
- build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?using
+ build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?typing_flags ?using
(Option.default (CAst.make @@ CRef (lt_ref,None)) r) m notations
| _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g ->
@@ -362,7 +367,7 @@ let do_fixpoint ~pm ~scope ~poly ?using l =
Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in
let fixkind = Declare.Obls.IsFixpoint annots in
let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in
- do_program_recursive ~pm ~scope ~poly ?using fixkind l
+ do_program_recursive ~pm ~scope ~poly ?typing_flags ?using fixkind l
| _, _ ->
CErrors.user_err ~hdr:"do_fixpoint"
(str "Well-founded fixpoints not allowed in mutually recursive blocks")
diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli
index 30bf3ae8f8..0193be8683 100644
--- a/vernac/comProgramFixpoint.mli
+++ b/vernac/comProgramFixpoint.mli
@@ -15,6 +15,7 @@ val do_fixpoint :
pm:Declare.OblState.t
-> scope:Locality.locality
-> poly:bool
+ -> ?typing_flags:Declarations.typing_flags
-> ?using:Vernacexpr.section_subset_expr
-> fixpoint_expr list
-> Declare.OblState.t
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 73ebca276d..fafee13bf6 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -83,14 +83,15 @@ module Info = struct
; udecl : UState.universe_decl
; scope : Locality.locality
; hook : Hook.t option
+ ; typing_flags : Declarations.typing_flags option
}
(** Note that [opaque] doesn't appear here as it is not known at the
start of the proof in the interactive case. *)
let make ?(poly=false) ?(inline=false) ?(kind=Decls.(IsDefinition Definition))
?(udecl=UState.default_univ_decl) ?(scope=Locality.Global Locality.ImportDefaultBehavior)
- ?hook () =
- { poly; inline; kind; udecl; scope; hook }
+ ?hook ?typing_flags () =
+ { poly; inline; kind; udecl; scope; hook; typing_flags }
end
@@ -325,12 +326,12 @@ let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proo
let feedback_axiom () = Feedback.(feedback AddedAxiom)
-let is_unsafe_typing_flags () =
+let is_unsafe_typing_flags flags =
+ let flags = Option.default (Global.typing_flags ()) flags in
let open Declarations in
- let flags = Environ.typing_flags (Global.env()) in
not (flags.check_universes && flags.check_guarded && flags.check_positive)
-let define_constant ~name cd =
+let define_constant ~name ~typing_flags cd =
(* Logically define the constant and its subproofs, no libobject tampering *)
let decl, unsafe = match cd with
| DefinitionEntry de ->
@@ -354,13 +355,13 @@ let define_constant ~name cd =
| PrimitiveEntry e ->
ConstantEntry (Entries.PrimitiveEntry e), false
in
- let kn = Global.add_constant name decl in
- if unsafe || is_unsafe_typing_flags() then feedback_axiom();
+ let kn = Global.add_constant ?typing_flags name decl in
+ if unsafe || is_unsafe_typing_flags typing_flags then feedback_axiom();
kn
-let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind cd =
+let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind ~typing_flags cd =
let () = check_exists name in
- let kn = define_constant ~name cd in
+ let kn = define_constant ~typing_flags ~name cd in
(* Register the libobjects attached to the constants *)
let () = register_constant kn kind local in
kn
@@ -557,7 +558,7 @@ let declare_definition_scheme ~internal ~univs ~role ~name c =
kn, eff
(* Locality stuff *)
-let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry =
+let declare_entry_core ~name ~scope ~kind ~typing_flags ?hook ~obls ~impargs ~uctx entry =
let should_suggest =
entry.proof_entry_opaque
&& not (List.is_empty (Global.named_context()))
@@ -570,7 +571,7 @@ let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry =
if should_suggest then Proof_using.suggest_variable (Global.env ()) name;
Names.GlobRef.VarRef name
| Locality.Global local ->
- let kn = declare_constant ~name ~local ~kind (DefinitionEntry entry) in
+ let kn = declare_constant ~name ~local ~kind ~typing_flags (DefinitionEntry entry) in
let gr = Names.GlobRef.ConstRef kn in
if should_suggest then Proof_using.suggest_constant (Global.env ()) kn;
let () = DeclareUniv.declare_univ_binders gr ubind in
@@ -583,10 +584,11 @@ let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry =
let declare_entry = declare_entry_core ~obls:[]
-let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes =
+let mutual_make_bodies ~typing_flags ~fixitems ~rec_declaration ~possible_indexes =
match possible_indexes with
| Some possible_indexes ->
let env = Global.env() in
+ let env = Environ.update_typing_flags ?typing_flags env in
let indexes = Pretyping.search_guard env possible_indexes rec_declaration in
let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),rec_declaration)) in
let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixitems in
@@ -597,9 +599,9 @@ let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes =
vars, fixdecls, None
let declare_mutually_recursive_core ~info ~cinfo ~opaque ~ntns ~uctx ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) () =
- let { Info.poly; udecl; scope; kind; _ } = info in
+ let { Info.poly; udecl; scope; kind; typing_flags; _ } = info in
let vars, fixdecls, indexes =
- mutual_make_bodies ~fixitems:cinfo ~rec_declaration ~possible_indexes in
+ mutual_make_bodies ~typing_flags ~fixitems:cinfo ~rec_declaration ~possible_indexes in
let uctx, univs =
(* XXX: Obligations don't do this, this seems like a bug? *)
if restrict_ucontext
@@ -614,7 +616,7 @@ let declare_mutually_recursive_core ~info ~cinfo ~opaque ~ntns ~uctx ~rec_declar
let csts = CList.map2
(fun CInfo.{ name; typ; impargs; using } body ->
let entry = definition_entry ~opaque ~types:typ ~univs ?using body in
- declare_entry ~name ~scope ~kind ~impargs ~uctx entry)
+ declare_entry ~name ~scope ~kind ~impargs ~uctx ~typing_flags entry)
cinfo fixdecls
in
let isfix = Option.has_some possible_indexes in
@@ -637,7 +639,7 @@ let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe =
in
let kind = Decls.(IsAssumption Conjectural) in
let decl = ParameterEntry pe in
- let kn = declare_constant ~name ~local ~kind decl in
+ let kn = declare_constant ~name ~local ~kind ~typing_flags:None decl in
let dref = Names.GlobRef.ConstRef kn in
let () = Impargs.maybe_declare_manual_implicits false dref impargs in
let () = assumption_message name in
@@ -680,8 +682,8 @@ let prepare_definition ~info ~opaque ?using ~body ~typ sigma =
let declare_definition_core ~info ~cinfo ~opaque ~obls ~body sigma =
let { CInfo.name; impargs; typ; using; _ } = cinfo in
let entry, uctx = prepare_definition ~info ~opaque ?using ~body ~typ sigma in
- let { Info.scope; kind; hook; _ } = info in
- declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry, uctx
+ let { Info.scope; kind; hook; typing_flags; _ } = info in
+ declare_entry_core ~name ~scope ~kind ~impargs ~typing_flags ~obls ?hook ~uctx entry, uctx
let declare_definition ~info ~cinfo ~opaque ~body sigma =
declare_definition_core ~obls:[] ~info ~cinfo ~opaque ~body sigma |> fst
@@ -913,6 +915,7 @@ let declare_obligation prg obl ~uctx ~types ~body =
(* ppedrot: seems legit to have obligations as local *)
let constant =
declare_constant ~name:obl.obl_name
+ ~typing_flags:prg.prg_info.Info.typing_flags
~local:Locality.ImportNeedQualified
~kind:Decls.(IsProof Property)
(DefinitionEntry ce)
@@ -1425,9 +1428,9 @@ let start_proof_core ~name ~typ ~pinfo ?(sign=initialize_named_context_for_proof
marked "opaque", this is a hack tho, see #10446, and
build_constant_by_tactic uses a different method that would break
program_inference_hook *)
- let { Proof_info.info = { Info.poly; _ }; _ } = pinfo in
+ let { Proof_info.info = { Info.poly; typing_flags; _ }; _ } = pinfo in
let goals = [Global.env_of_context sign, typ] in
- let proof = Proof.start ~name ~poly sigma goals in
+ let proof = Proof.start ~name ~poly ?typing_flags sigma goals in
let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
{ proof
; endline_tactic = None
@@ -1448,7 +1451,8 @@ let start_core ~info ~cinfo ?proof_ending sigma =
let start = start_core ?proof_ending:None
let start_dependent ~info ~name ~proof_ending goals =
- let proof = Proof.dependent_start ~name ~poly:info.Info.poly goals in
+ let { Info.poly; typing_flags; _ } = info in
+ let proof = Proof.dependent_start ~name ~poly ?typing_flags goals in
let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
let cinfo = [] in
let pinfo = Proof_info.make ~info ~cinfo ~proof_ending () in
@@ -1886,7 +1890,7 @@ end = struct
let declare_mutdef ~uctx ~pinfo pe i CInfo.{ name; impargs; typ; _} =
let { Proof_info.info; compute_guard; _ } = pinfo in
- let { Info.hook; scope; kind; _ } = info in
+ let { Info.hook; scope; kind; typing_flags; _ } = info in
(* if i = 0 , we don't touch the type; this is for compat
but not clear it is the right thing to do.
*)
@@ -1903,7 +1907,7 @@ end = struct
Internal.map_entry_body pe
~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff)
in
- declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe
+ declare_entry ~name ~scope ~kind ?hook ~impargs ~typing_flags ~uctx pe
let declare_mutdef ~pinfo ~uctx ~entry =
let pe = match pinfo.Proof_info.compute_guard with
@@ -1913,6 +1917,8 @@ end = struct
| possible_indexes ->
(* Try all combinations... not optimal *)
let env = Global.env() in
+ let typing_flags = pinfo.Proof_info.info.Info.typing_flags in
+ let env = Environ.update_typing_flags ?typing_flags env in
Internal.map_entry_body entry
~f:(guess_decreasing env possible_indexes)
in
@@ -1993,7 +1999,7 @@ let finish_derived ~f ~name ~entries =
let f_def = Internal.set_opacity ~opaque:false f_def in
let f_kind = Decls.(IsDefinition Definition) in
let f_def = DefinitionEntry f_def in
- let f_kn = declare_constant ~name:f ~kind:f_kind f_def in
+ let f_kn = declare_constant ~name:f ~kind:f_kind f_def ~typing_flags:None in
let f_kn_term = Constr.mkConst f_kn in
(* In the type and body of the proof of [suchthat] there can be
references to the variable [f]. It needs to be replaced by
@@ -2011,7 +2017,7 @@ let finish_derived ~f ~name ~entries =
(* The same is done in the body of the proof. *)
let lemma_def = Internal.map_entry_body lemma_def ~f:(fun ((b,ctx),fx) -> (substf b, ctx), fx) in
let lemma_def = DefinitionEntry lemma_def in
- let ct = declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in
+ let ct = declare_constant ~name ~typing_flags:None ~kind:Decls.(IsProof Proposition) lemma_def in
[GlobRef.ConstRef f_kn; GlobRef.ConstRef ct]
let finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma0 =
@@ -2025,7 +2031,7 @@ let finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma0 =
| None -> let n = !obls in incr obls; Nameops.add_suffix i ("_obligation_" ^ string_of_int n)
in
let entry, args = Internal.shrink_entry local_context entry in
- let cst = declare_constant ~name:id ~kind (DefinitionEntry entry) in
+ let cst = declare_constant ~name:id ~kind ~typing_flags:None (DefinitionEntry entry) in
let sigma, app = Evarutil.new_global sigma (GlobRef.ConstRef cst) in
let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in
sigma, cst) sigma0
@@ -2519,3 +2525,9 @@ type nonrec progress = progress =
end
module OblState = Obls_.State
+
+let declare_constant ?local ~name ~kind ?typing_flags =
+ declare_constant ?local ~name ~kind ~typing_flags
+
+let declare_entry ~name ~scope ~kind =
+ declare_entry ~name ~scope ~kind ~typing_flags:None
diff --git a/vernac/declare.mli b/vernac/declare.mli
index e4c77113af..37a61cc4f0 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -109,6 +109,7 @@ module Info : sig
(** locality *)
-> ?hook : Hook.t
(** Callback to be executed after saving the constant *)
+ -> ?typing_flags:Declarations.typing_flags
-> unit
-> t
@@ -387,6 +388,7 @@ val declare_constant
: ?local:Locality.import_status
-> name:Id.t
-> kind:Decls.logical_kind
+ -> ?typing_flags:Declarations.typing_flags
-> Evd.side_effects constant_entry
-> Constant.t
diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml
index e22d63b811..7050ddc042 100644
--- a/vernac/declareInd.ml
+++ b/vernac/declareInd.ml
@@ -104,7 +104,7 @@ let is_unsafe_typing_flags () =
not (flags.check_universes && flags.check_guarded && flags.check_positive)
(* for initial declaration *)
-let declare_mind mie =
+let declare_mind ?typing_flags mie =
let id = match mie.mind_entry_inds with
| ind::_ -> ind.mind_entry_typename
| [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in
@@ -113,7 +113,7 @@ let declare_mind mie =
List.iter (fun (typ, cons) ->
Declare.check_exists typ;
List.iter Declare.check_exists cons) names;
- let _kn' = Global.add_mind id mie in
+ let _kn' = Global.add_mind ?typing_flags id mie in
let (sp,kn as oname) = Lib.add_leaf id (inInductive { ind_names = names }) in
if is_unsafe_typing_flags() then feedback_axiom ();
let mind = Global.mind_of_delta_kn kn in
@@ -154,7 +154,7 @@ type one_inductive_impls =
Impargs.manual_implicits (* for inds *) *
Impargs.manual_implicits list (* for constrs *)
-let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie pl impls =
+let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) ?typing_flags 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
@@ -166,7 +166,7 @@ let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie p
| _ -> ()
end;
let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
- let (_, kn), prim = declare_mind mie in
+ let (_, kn), prim = declare_mind ?typing_flags mie in
let mind = Global.mind_of_delta_kn kn in
if primitive_expected && not prim then warn_non_primitive_record (mind,0);
DeclareUniv.declare_univ_binders (GlobRef.IndRef (mind,0)) pl;
diff --git a/vernac/declareInd.mli b/vernac/declareInd.mli
index 05a1617329..eacf20e30c 100644
--- a/vernac/declareInd.mli
+++ b/vernac/declareInd.mli
@@ -17,6 +17,7 @@ type one_inductive_impls =
val declare_mutual_inductive_with_eliminations
: ?primitive_expected:bool
+ -> ?typing_flags:Declarations.typing_flags
-> Entries.mutual_inductive_entry
-> UnivNames.universe_binders
-> one_inductive_impls list
diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
index 1705915e70..1987d48e0f 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -109,9 +109,8 @@ let do_universe ~poly l =
let do_constraint ~poly l =
let open Univ in
- let u_of_id x =
- Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x
- in
+ let evd = Evd.from_env (Global.env ()) in
+ let u_of_id x = Constrintern.interp_known_level evd x in
let constraints = List.fold_left (fun acc (l, d, r) ->
let lu = u_of_id l and ru = u_of_id r in
Constraint.add (lu, d, ru) acc)
diff --git a/vernac/declareUniv.mli b/vernac/declareUniv.mli
index e4d1d5dc65..ca990a58eb 100644
--- a/vernac/declareUniv.mli
+++ b/vernac/declareUniv.mli
@@ -17,4 +17,4 @@ exception AlreadyDeclared of (string option * Id.t)
val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
val do_universe : poly:bool -> lident list -> unit
-val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit
+val do_constraint : poly:bool -> Constrexpr.univ_constraint_expr list -> unit
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 9d86ea90e6..d35e13c4ef 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -572,6 +572,13 @@ let rec explain_evar_kind env sigma evk ty =
strbrk "the type of " ++ Id.print id
| Evar_kinds.BinderType Anonymous ->
strbrk "the type of this anonymous binder"
+ | Evar_kinds.EvarType (ido,evk) ->
+ let pp = match ido with
+ | Some id -> str "?" ++ Id.print id
+ | None ->
+ try pr_existential_key sigma evk
+ with (* defined *) Not_found -> strbrk "an internal placeholder" in
+ strbrk "the type of " ++ pp
| Evar_kinds.ImplicitArg (c,(n,ido),b) ->
let id = Option.get ido in
strbrk "the implicit parameter " ++ Id.print id ++ spc () ++ str "of" ++
@@ -961,7 +968,7 @@ let explain_not_match_error = function
status (not b) ++ str" declaration was found"
| IncompatibleUniverses incon ->
str"the universe constraints are inconsistent: " ++
- Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes incon
+ Univ.explain_universe_inconsistency UnivNames.(pr_with_global_universes empty_binders) incon
| IncompatiblePolymorphism (env, t1, t2) ->
str "conversion of polymorphic values generates additional constraints: " ++
quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t1) ++ spc () ++
@@ -1218,7 +1225,7 @@ let error_large_non_prop_inductive_not_in_type () =
str "Large non-propositional inductive types must be in Type."
let error_inductive_missing_constraints (us,ind_univ) =
- let pr_u = Univ.Universe.pr_with UnivNames.pr_with_global_universes in
+ let pr_u = Univ.Universe.pr_with UnivNames.(pr_with_global_universes empty_binders) in
str "Missing universe constraint declared for inductive type:" ++ spc()
++ v 0 (prlist_with_sep spc (fun u ->
hov 0 (pr_u u ++ str " <= " ++ pr_u ind_univ))
@@ -1406,7 +1413,7 @@ let _ = CErrors.register_handler (wrap_unhandled explain_exn_default)
let rec vernac_interp_error_handler = function
| Univ.UniverseInconsistency i ->
str "Universe inconsistency." ++ spc() ++
- Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i ++ str "."
+ Univ.explain_universe_inconsistency UnivNames.(pr_with_global_universes empty_binders) i ++ str "."
| TypeError(ctx,te) ->
let te = map_ptype_error EConstr.of_constr te in
explain_type_error ctx Evd.empty te
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 01873918aa..ff4365c8d3 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -60,8 +60,8 @@ let pr_red_expr =
keyword
let pr_uconstraint (l, d, r) =
- pr_glob_sort_name l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
- pr_glob_sort_name r
+ pr_sort_name_expr l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
+ pr_sort_name_expr r
let pr_univ_name_list = function
| None -> mt ()
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 840754ccc6..0fc6c7f87b 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -206,7 +206,7 @@ let print_if_is_coercion ref =
let pr_template_variables = function
| [] -> mt ()
- | vars -> str "on " ++ prlist_with_sep spc UnivNames.pr_with_global_universes vars
+ | vars -> str "on " ++ prlist_with_sep spc UnivNames.(pr_with_global_universes empty_binders) vars
let print_polymorphism ref =
let poly = Global.is_polymorphic ref in
@@ -668,7 +668,7 @@ let gallina_print_syntactic_def env kn =
spc () ++ str ":=") ++
spc () ++
Constrextern.without_specific_symbols
- [Notation.SynDefRule kn] (pr_glob_constr_env env) c)
+ [Notation.SynDefRule kn] (pr_glob_constr_env env (Evd.from_env env)) c)
module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> Pp.t option end)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0f63dfe5ce..a3726daf63 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -57,16 +57,17 @@ module DefAttributes = struct
program : bool;
deprecated : Deprecation.t option;
canonical_instance : bool;
+ typing_flags : Declarations.typing_flags option;
using : Vernacexpr.section_subset_expr option;
}
let parse f =
let open Attributes in
- let ((((locality, deprecated), polymorphic), program), canonical_instance), using =
- parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance ++ using) f
+ let (((((locality, deprecated), polymorphic), program), canonical_instance), typing_flags), using =
+ parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance ++ typing_flags ++ using) f
in
let using = Option.map Proof_using.using_from_string using in
- { polymorphic; program; locality; deprecated; canonical_instance; using }
+ { polymorphic; program; locality; deprecated; canonical_instance; typing_flags; using }
end
let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l))
@@ -353,9 +354,9 @@ let universe_subgraph ?loc kept univ =
let open Univ in
let sigma = Evd.from_env (Global.env()) in
let parse q =
- let q = Glob_term.(GType q) in
+ let q = Constrexpr.CType q in
(* this function has a nice error message for not found univs *)
- Pretyping.interp_known_glob_level ?loc sigma q
+ Constrintern.interp_known_level sigma q
in
let kept = List.fold_left (fun kept q -> LSet.add (parse q) kept) LSet.empty kept in
let csts = UGraph.constraints_for ~kept univ in
@@ -377,7 +378,7 @@ let print_universes ?loc ~sort ~subgraph dst =
if Global.is_joined_environment () then mt ()
else str"There may remain asynchronous universe constraints"
in
- let prl = UnivNames.pr_with_global_universes in
+ let prl = UnivNames.(pr_with_global_universes empty_binders) in
begin match dst with
| None -> UGraph.pr_universes prl univ ++ pr_remaining
| Some s -> dump_universes_gen (fun u -> Pp.string_of_ppcmds (prl u)) univ s
@@ -512,6 +513,7 @@ let vernac_set_used_variables ~pstate e : Declare.Proof.t =
l;
let _, pstate = Declare.Proof.set_used_variables pstate l in
pstate
+
let vernac_set_used_variables_opt ?using pstate =
match using with
| None -> pstate
@@ -546,28 +548,29 @@ let post_check_evd ~udecl ~poly evd =
else (* We fix the variables to ensure they won't be lowered to Set *)
Evd.fix_undefined_variables evd
-let start_lemma_com ~program_mode ~poly ~scope ~kind ?using ?hook thms =
+let start_lemma_com ~typing_flags ~program_mode ~poly ~scope ~kind ?using ?hook thms =
let env0 = Global.env () in
+ let env0 = Environ.update_typing_flags ?typing_flags env0 in
let flags = Pretyping.{ all_no_fail_flags with program_mode } in
let decl = fst (List.hd thms) in
let evd, udecl = Constrintern.interp_univ_decl_opt env0 (snd decl) in
let evd, thms = interp_lemma ~program_mode ~flags ~scope env0 evd thms in
let mut_analysis = RecLemmas.look_for_possibly_mutual_statements evd thms in
let evd = Evd.minimize_universes evd in
- let pstate =
+ let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl ?typing_flags () in
+ begin
match mut_analysis with
| RecLemmas.NonMutual thm ->
let thm = Declare.CInfo.to_constr evd thm in
let evd = post_check_evd ~udecl ~poly evd in
- let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
Declare.Proof.start_with_initialization ~info ~cinfo:thm evd
| RecLemmas.Mutual { mutual_info; cinfo ; possible_guards } ->
let cinfo = List.map (Declare.CInfo.to_constr evd) cinfo in
let evd = post_check_evd ~udecl ~poly evd in
- let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
Declare.Proof.start_mutual_with_initialization ~info ~cinfo evd ~mutual_info (Some possible_guards)
- in
- vernac_set_used_variables_opt ?using pstate
+ end
+ (* XXX: This should be handled in start_with_initialization, see duplicate using in declare.ml *)
+ |> vernac_set_used_variables_opt ?using
let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function
| Coercion ->
@@ -606,14 +609,16 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in
let program_mode = atts.program in
let poly = atts.polymorphic in
+ let typing_flags = atts.typing_flags in
let name = vernac_definition_name lid local in
- start_lemma_com ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?using:atts.using ?hook [(name, pl), (bl, t)]
+ start_lemma_com ~typing_flags ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?using:atts.using ?hook [(name, pl), (bl, t)]
let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_opt =
let open DefAttributes in
let scope = enforce_locality_exp atts.locality discharge in
let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in
let program_mode = atts.program in
+ let typing_flags = atts.typing_flags in
let name = vernac_definition_name lid scope in
let red_option = match red_option with
| None -> None
@@ -624,11 +629,11 @@ let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_
if program_mode then
let kind = Decls.IsDefinition kind in
ComDefinition.do_definition_program ~pm ~name:name.v
- ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook
+ ~poly:atts.polymorphic ?typing_flags ~scope ~kind pl bl red_option c typ_opt ?hook
else
let () =
ComDefinition.do_definition ~name:name.v
- ~poly:atts.polymorphic ~scope ~kind ?using:atts.using pl bl red_option c typ_opt ?hook in
+ ~poly:atts.polymorphic ?typing_flags ~scope ~kind ?using:atts.using pl bl red_option c typ_opt ?hook in
pm
(* NB: pstate argument to use combinators easily *)
@@ -637,7 +642,11 @@ let vernac_start_proof ~atts kind l =
let scope = enforce_locality_exp atts.locality NoDischarge in
if Dumpglob.dump () then
List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
- start_lemma_com ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) ?using:atts.using l
+ start_lemma_com
+ ~typing_flags:atts.typing_flags
+ ~program_mode:atts.program
+ ~poly:atts.polymorphic
+ ~scope ~kind:(Decls.IsProof kind) ?using:atts.using l
let vernac_end_proof ~lemma ~pm = let open Vernacexpr in function
| Admitted ->
@@ -720,7 +729,7 @@ let should_treat_as_uniform () =
then ComInductive.UniformParameters
else ComInductive.NonUniformParameters
-let vernac_record ~template udecl ~cumulative k ~poly finite records =
+let vernac_record ~template udecl ~cumulative k ~poly ?typing_flags finite records =
let map ((is_coercion, name), binders, sort, nameopt, cfs) =
let idbuild = match nameopt with
| None -> Nameops.add_prefix "Build_" name.v
@@ -741,7 +750,13 @@ let vernac_record ~template udecl ~cumulative k ~poly finite records =
Record.Ast.{ name; is_coercion; binders; cfs; idbuild; sort }
in
let records = List.map map records in
- ignore(Record.definition_structure ~template udecl k ~cumulative ~poly finite records)
+ match typing_flags with
+ | Some _ ->
+ CErrors.user_err (Pp.str "typing flags are not yet supported for records")
+ | None ->
+ let _ : _ list =
+ Record.definition_structure ~template udecl k ~cumulative ~poly finite records in
+ ()
let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) =
match indl with
@@ -773,8 +788,8 @@ let private_ind =
| None -> return false
let vernac_inductive ~atts kind indl =
- let (template, (poly, cumulative)), private_ind = Attributes.(
- parse Notations.(template ++ polymorphic_cumulative ++ private_ind) atts) in
+ let ((template, (poly, cumulative)), private_ind), typing_flags = Attributes.(
+ parse Notations.(template ++ polymorphic_cumulative ++ private_ind ++ typing_flags) atts) in
let open Pp in
let udecl, indl = extract_inductive_udecl indl in
if Dumpglob.dump () then
@@ -811,7 +826,7 @@ let vernac_inductive ~atts kind indl =
let coe' = if coe then BackInstance else NoInstance in
let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), [], ce),
{ rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in
- vernac_record ~template udecl ~cumulative (Class true) ~poly finite [id, bl, c, None, [f]]
+ vernac_record ~template udecl ~cumulative (Class true) ~poly ?typing_flags finite [id, bl, c, None, [f]]
else if List.for_all is_record indl then
(* Mutual record case *)
let () = match kind with
@@ -836,7 +851,7 @@ let vernac_inductive ~atts kind indl =
in
let kind = match kind with Class _ -> Class false | _ -> kind in
let recordl = List.map unpack indl in
- vernac_record ~template udecl ~cumulative kind ~poly finite recordl
+ vernac_record ~template udecl ~cumulative kind ~poly ?typing_flags finite recordl
else if List.for_all is_constructor indl then
(* Mutual inductive case *)
let () = match kind with
@@ -860,7 +875,7 @@ let vernac_inductive ~atts kind indl =
in
let indl = List.map unpack indl in
let uniform = should_treat_as_uniform () in
- ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uniform finite
+ ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ?typing_flags ~private_ind ~uniform finite
else
user_err (str "Mixed record-inductive definitions are not allowed")
@@ -874,17 +889,19 @@ let vernac_fixpoint_interactive ~atts discharge l =
let scope = vernac_fixpoint_common ~atts discharge l in
if atts.program then
CErrors.user_err Pp.(str"Program Fixpoint requires a body");
- vernac_set_used_variables_opt ?using:atts.using
- (ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic l)
+ let typing_flags = atts.typing_flags in
+ ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic ?typing_flags l
+ |> vernac_set_used_variables_opt ?using:atts.using
let vernac_fixpoint ~atts ~pm discharge l =
let open DefAttributes in
let scope = vernac_fixpoint_common ~atts discharge l in
+ let typing_flags = atts.typing_flags in
if atts.program then
(* XXX: Switch to the attribute system and match on ~atts *)
- ComProgramFixpoint.do_fixpoint ~pm ~scope ~poly:atts.polymorphic ?using:atts.using l
+ ComProgramFixpoint.do_fixpoint ~pm ~scope ~poly:atts.polymorphic ?typing_flags ?using:atts.using l
else
- let () = ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic ?using:atts.using l in
+ let () = ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic ?typing_flags ?using:atts.using l in
pm
let vernac_cofixpoint_common ~atts discharge l =
@@ -1829,11 +1846,11 @@ let vernac_print ~pstate =
| PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s
| PrintHintDb -> Hints.pr_searchtable env sigma
| PrintScopes ->
- Notation.pr_scopes (Constrextern.without_symbols (pr_glob_constr_env env))
+ Notation.pr_scopes (Constrextern.without_symbols (pr_glob_constr_env env sigma))
| PrintScope s ->
- Notation.pr_scope (Constrextern.without_symbols (pr_glob_constr_env env)) s
+ Notation.pr_scope (Constrextern.without_symbols (pr_glob_constr_env env sigma)) s
| PrintVisibility s ->
- Notation.pr_visibility (Constrextern.without_symbols (pr_glob_constr_env env)) s
+ Notation.pr_visibility (Constrextern.without_symbols (pr_glob_constr_env env sigma)) s
| PrintAbout (ref_or_by_not,udecl,glnumopt) ->
print_about_hyp_globs ~pstate ref_or_by_not udecl glnumopt
| PrintImplicit qid ->
@@ -1867,9 +1884,9 @@ let vernac_locate ~pstate = let open Constrexpr in function
| LocateTerm {v=AN qid} -> Prettyp.print_located_term qid
| LocateAny {v=ByNotation (ntn, sc)} (* TODO : handle Ltac notations *)
| LocateTerm {v=ByNotation (ntn, sc)} ->
- let _, env = get_current_or_global_context ~pstate in
+ let sigma, env = get_current_or_global_context ~pstate in
Notation.locate_notation
- (Constrextern.without_symbols (pr_glob_constr_env env)) ntn sc
+ (Constrextern.without_symbols (pr_glob_constr_env env sigma)) ntn sc
| LocateLibrary qid -> print_located_library qid
| LocateModule qid -> Prettyp.print_located_module qid
| LocateOther (s, qid) -> Prettyp.print_located_other s qid
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index defb0691c0..2e360cf969 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -129,8 +129,6 @@ type option_setting =
(** Identifier and optional list of bound universes and constraints. *)
-type sort_expr = Sorts.family
-
type definition_expr =
| ProveBody of local_binder_expr list * constr_expr
| DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr
@@ -210,8 +208,8 @@ type proof_end =
| Proved of opacity_flag * lident option
type scheme =
- | InductionScheme of bool * qualid or_by_notation * sort_expr
- | CaseScheme of bool * qualid or_by_notation * sort_expr
+ | InductionScheme of bool * qualid or_by_notation * Sorts.family
+ | CaseScheme of bool * qualid or_by_notation * Sorts.family
| EqualityScheme of qualid or_by_notation
type section_subset_expr =
@@ -341,7 +339,7 @@ type nonrec vernac_expr =
| VernacScheme of (lident option * scheme) list
| VernacCombinedScheme of lident * lident list
| VernacUniverse of lident list
- | VernacConstraint of Glob_term.glob_constraint list
+ | VernacConstraint of univ_constraint_expr list
(* Gallina extensions *)
| VernacBeginSection of lident
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 03:01:19 +0000