diff options
43 files changed, 322 insertions, 265 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 2947bfb700..45597851ef 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -229,7 +229,6 @@ windows64: <<: *windows-template variables: ARCH: "64" - allow_failure: true windows32: <<: *windows-template @@ -237,7 +236,6 @@ windows32: ARCH: "32" except: - /^pr-.*$/ - allow_failure: true pkg:opam: stage: test diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index d0b5f4be47..b202635714 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1905,6 +1905,9 @@ function make_addon_quickchick { function make_addons { # Note: ':' is the empty command, which does not produce any output : > "/build/filelists/addon_dependencies.nsh" + : > "/build/filelists/addon_strings.nsh" + : > "/build/filelists/addon_descriptions.nsh" + : > "/build/filelists/addon_sections.nsh" for addon in $COQ_ADDONS; do "make_addon_$addon" diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat index 918d289ae2..386a3de204 100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -39,6 +39,10 @@ SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\ IF "%WINDOWS%" == "enabled_all_addons" (
SET EXTRA_ADDONS=^
+ -addon=bignums ^
+ -addon=equations ^
+ -addon=ltac2 ^
+ -addon=mtac2 ^
-addon=mathcomp ^
-addon=menhir ^
-addon=menhirlib ^
@@ -56,10 +60,6 @@ IF "%WINDOWS%" == "enabled_all_addons" ( call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
-arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
-destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
- -addon=bignums ^
- -addon=equations ^
- -addon=ltac2 ^
- -addon=mtac2 ^
%EXTRA_ADDONS% ^
-make=N ^
-setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 15a55d9e72..882798205b 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -260,6 +260,12 @@ preorder can be used instead. This is very similar to the coercion mechanism of ``Structure`` declarations. The implementation simply declares each projection as an instance. +.. warn:: Ignored instance declaration for “@ident”: “@term” is not a class + + Using this ``:>`` syntax with a right-hand-side that is not itself a Class + has no effect (apart from emitting this warning). In particular, is does not + declare a coercion. + One can also declare existing objects or structure projections using the Existing Instance command to achieve the same effect. diff --git a/engine/namegen.ml b/engine/namegen.ml index 0f346edd3e..a67ff6965b 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -208,23 +208,16 @@ let it_mkLambda_or_LetIn_name env sigma b hyps = (* Introduce a mode where auto-generated names are mangled to test dependence of scripts on auto-generated names *) -let mangle_names = ref false - -let () = Goptions.( - declare_bool_option - { optdepr = false; - optname = "mangle auto-generated names"; - optkey = ["Mangle";"Names"]; - optread = (fun () -> !mangle_names); - optwrite = (:=) mangle_names; }) +let get_mangle_names = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"mangle auto-generated names" + ~key:["Mangle";"Names"] + ~value:false let mangle_names_prefix = ref (Id.of_string "_0") -let set_prefix x = mangle_names_prefix := forget_subscript x -let set_mangle_names_mode x = begin - set_prefix x; - mangle_names := true - end +let set_prefix x = mangle_names_prefix := forget_subscript x let () = Goptions.( declare_string_option @@ -238,7 +231,7 @@ let () = Goptions.( with CErrors.UserError _ -> CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\"."))) end }) -let mangle_id id = if !mangle_names then !mangle_names_prefix else id +let mangle_id id = if get_mangle_names () then !mangle_names_prefix else id (* Looks for next "good" name by lifting subscript *) diff --git a/engine/namegen.mli b/engine/namegen.mli index a53c3a0d1f..3722cbed24 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -125,7 +125,3 @@ val rename_bound_vars_as_displayed : val compute_displayed_name_in_gen : (evar_map -> int -> 'a -> bool) -> evar_map -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t - -val set_mangle_names_mode : Id.t -> unit -(** Turn on mangled names mode and with the given prefix. - @raise UserError if the argument is invalid as an identifier. *) diff --git a/engine/uState.ml b/engine/uState.ml index 5b0671c06e..6aecc368e6 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -577,25 +577,33 @@ let add_global_univ uctx u = uctx_universes = univs } let make_flexible_variable ctx ~algebraic u = - let {uctx_local = cstrs; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in - let uvars' = Univ.LMap.add u None uvars in - let avars' = - if algebraic then - let uu = Univ.Universe.make u in - let substu_not_alg u' v = - Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v - in - let has_upper_constraint () = - Univ.Constraint.exists - (fun (l,d,r) -> d == Univ.Lt && Univ.Level.equal l u) - (Univ.ContextSet.constraints cstrs) - in - if not (Univ.LMap.exists substu_not_alg uvars || has_upper_constraint ()) - then Univ.LSet.add u avars else avars - else avars - in - {ctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = avars'} + let open Univ in + let {uctx_local = cstrs; uctx_univ_variables = uvars; + uctx_univ_algebraic = avars; uctx_universes=g; } = ctx in + assert (try LMap.find u uvars == None with Not_found -> true); + match UGraph.choose (fun v -> not (Level.equal u v) && (algebraic || not (LSet.mem v avars))) g u with + | Some v -> + let uvars' = LMap.add u (Some (Universe.make v)) uvars in + { ctx with uctx_univ_variables = uvars'; } + | None -> + let uvars' = LMap.add u None uvars in + let avars' = + if algebraic then + let uu = Universe.make u in + let substu_not_alg u' v = + Option.cata (fun vu -> Universe.equal uu vu && not (LSet.mem u' avars)) false v + in + let has_upper_constraint () = + Constraint.exists + (fun (l,d,r) -> d == Lt && Level.equal l u) + (ContextSet.constraints cstrs) + in + if not (LMap.exists substu_not_alg uvars || has_upper_constraint ()) + then LSet.add u avars else avars + else avars + in + {ctx with uctx_univ_variables = uvars'; + uctx_univ_algebraic = avars'} let make_nonalgebraic_variable ctx u = { ctx with uctx_univ_algebraic = Univ.LSet.remove u ctx.uctx_univ_algebraic } diff --git a/engine/univMinim.ml b/engine/univMinim.ml index 68c2724f26..e20055b133 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -12,17 +12,12 @@ open Univ open UnivSubst (* To disallow minimization to Set *) -let set_minimization = ref true -let is_set_minimization () = !set_minimization - -let () = - Goptions.(declare_bool_option - { optdepr = false; - optname = "minimization to Set"; - optkey = ["Universe";"Minimization";"ToSet"]; - optread = is_set_minimization; - optwrite = (:=) set_minimization }) - +let get_set_minimization = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"minimization to Set" + ~key:["Universe";"Minimization";"ToSet"] + ~value:true (** Simplification *) @@ -278,7 +273,7 @@ let normalize_context_set g ctx us algs weak = let smallles, csts = Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts in - let smallles = if is_set_minimization () + let smallles = if get_set_minimization () then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles else Constraint.empty in diff --git a/ide/idetop.ml b/ide/idetop.ml index 8cb02190e6..a2b85041e8 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -537,5 +537,5 @@ let islave_init ~opts extra_args = let () = let open Coqtop in - let custom = { init = islave_init; run = loop; } in + let custom = { init = islave_init; run = loop; opts = Coqargs.default_opts } in start_coq custom diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 07ed7825ff..3a4969a3ee 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -604,15 +604,6 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function CErrors.user_err ?loc ~hdr:"coerce_to_cases_pattern_expr" (str "This expression should be coercible to a pattern.")) c -let asymmetric_patterns = ref (false) -let () = Goptions.(declare_bool_option { - optdepr = false; - optname = "no parameters in constructors"; - optkey = ["Asymmetric";"Patterns"]; - optread = (fun () -> !asymmetric_patterns); - optwrite = (fun a -> asymmetric_patterns:=a); -}) - (** Local universe and constraint declarations. *) let interp_univ_constraints env evd cstrs = diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 9e83bde8b2..7f14eb4583 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -127,9 +127,6 @@ val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> notation - (** For cases pattern parsing errors *) val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a -(** Placeholder for global option, should be moved to a parameter *) -val asymmetric_patterns : bool ref - (** Local universe and constraint declarations. *) val interp_univ_decl : Environ.env -> universe_decl_expr -> Evd.evar_map * UState.universe_decl diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0f5fa14c23..25f2526f74 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -193,17 +193,12 @@ let without_specific_symbols l = (* Control printing of records *) (* Set Record Printing flag *) -let record_print = ref true - -let () = - let open Goptions in - declare_bool_option - { optdepr = false; - optname = "record printing"; - optkey = ["Printing";"Records"]; - optread = (fun () -> !record_print); - optwrite = (fun b -> record_print := b) } - +let get_record_print = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"record printing" + ~key:["Printing";"Records"] + ~value:true let is_record indsp = try @@ -431,7 +426,7 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = with Not_found | No_match | Exit -> let c = extern_reference Id.Set.empty (ConstructRef cstrsp) in - if !asymmetric_patterns then + if Constrintern.get_asymmetric_patterns () then if pattern_printable_in_both_syntax cstrsp then CPatCstr (c, None, args) else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) @@ -469,7 +464,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) List.map (extern_cases_pattern_in_scope subscope vars) c) substlist in let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in - let l2' = if !asymmetric_patterns || not (List.is_empty ll) then l2 + let l2' = if Constrintern.get_asymmetric_patterns () || not (List.is_empty ll) then l2 else match drop_implicits_in_patt gr nb_to_drop l2 with |Some true_args -> true_args @@ -489,7 +484,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c) subst in let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in - let l2' = if !asymmetric_patterns then l2 + let l2' = if Constrintern.get_asymmetric_patterns () then l2 else match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with |Some true_args -> true_args @@ -824,7 +819,7 @@ let rec extern inctx scopes vars r = () else if PrintingConstructor.active (fst cstrsp) then raise Exit - else if not !record_print then + else if not (get_record_print ()) then raise Exit; let projs = struc.Recordops.s_PROJ in let locals = struc.Recordops.s_PROJKIND in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 02db8f6aab..6313f2d7ba 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1488,6 +1488,12 @@ let is_non_zero_pat c = match c with | { CAst.v = CPatPrim (Numeral (p, true)) } -> not (is_zero p) | _ -> false +let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"no parameters in constructors" + ~key:["Asymmetric";"Patterns"] + ~value:false + let drop_notations_pattern looked_for genv = (* At toplevel, Constructors and Inductives are accepted, in recursive calls only constructor are allowed *) @@ -1562,7 +1568,7 @@ let drop_notations_pattern looked_for genv = | None -> DAst.make ?loc @@ RCPatAtom None | Some (n, head, pl) -> let pl = - if !asymmetric_patterns then pl else + if get_asymmetric_patterns () then pl else let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in List.rev_append pars pl in match drop_syndef top scopes head pl with @@ -1684,7 +1690,7 @@ let rec intern_pat genv ntnvars aliases pat = let aliases' = merge_aliases aliases id in intern_pat genv ntnvars aliases' p | RCPatCstr (head, expl_pl, pl) -> - if !asymmetric_patterns then + if get_asymmetric_patterns () then let len = if List.is_empty expl_pl then Some (List.length pl) else None in let c,idslpl1 = find_constructor loc len head in let with_letin = diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 147a903fe2..035e4bc644 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -197,3 +197,6 @@ val parsing_explicit : bool ref (** Globalization leak for Grammar *) val for_grammar : ('a -> 'b) -> 'a -> 'b + +(** Placeholder for global option, should be moved to a parameter *) +val get_asymmetric_patterns : unit -> bool diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index fe07a1c90e..afdc8f1511 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -868,6 +868,21 @@ let constraints_for ~kept g = let domain g = LMap.domain g.entries +let choose p g u = + let exception Found of Level.t in + let ru = (repr g u).univ in + if p ru then Some ru + else + try LMap.iter (fun v -> function + | Canonical _ -> () (* we already tried [p ru] *) + | Equiv v' -> + let rv = (repr g v').univ in + if rv == ru && p v then raise (Found v) + (* NB: we could also try [p v'] but it will come up in the + rest of the iteration regardless. *) + ) g.entries; None + with Found v -> Some v + (** [sort_universes g] builds a totally ordered universe graph. The output graph should imply the input graph (and the implication will be strict most of the time), but is not necessarily minimal. diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index a389b35993..4dbfac5c73 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -73,6 +73,10 @@ val sort_universes : t -> t of the universes into equivalence classes. *) val constraints_of_universes : t -> Constraint.t * LSet.t list +val choose : (Level.t -> bool) -> t -> Level.t -> Level.t option +(** [choose p g u] picks a universe verifying [p] and equal + to [u] in [g]. *) + (** [constraints_for ~kept g] returns the constraints about the universes [kept] in [g] up to transitivity. diff --git a/lib/flags.ml b/lib/flags.ml index 3aef5a7b2c..ae4d337ded 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -123,8 +123,5 @@ let get_inline_level () = !inline_level (* Native code compilation for conversion and normalization *) let output_native_objects = ref false -(* Print the mod uid associated to a vo file by the native compiler *) -let print_mod_uid = ref false - let profile_ltac = ref false let profile_ltac_cutoff = ref 2.0 diff --git a/lib/flags.mli b/lib/flags.mli index e282d4ca8c..d883cf1e30 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -119,8 +119,6 @@ val default_inline_level : int (** When producing vo objects, also compile the native-code version *) val output_native_objects : bool ref -(** Print the mod uid associated to a vo file by the native compiler *) -val print_mod_uid : bool ref - +(** Global profile_ltac flag *) val profile_ltac : bool ref val profile_ltac_cutoff : float ref diff --git a/library/goptions.ml b/library/goptions.ml index bb9b4e29fc..98efb512ab 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -299,6 +299,18 @@ let declare_stringopt_option = (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option.")) (fun _ _ -> anomaly (Pp.str "async_option.")) +let declare_bool_option_and_ref ~depr ~name ~key ~(value:bool) = + let r_opt = ref value in + let optwrite v = r_opt := v in + let optread () = !r_opt in + let _ = declare_bool_option { + optdepr = depr; + optname = name; + optkey = key; + optread; optwrite + } in + optread + (* 3- User accessible commands *) (* Setting values of options *) @@ -422,6 +434,3 @@ let print_tables () = (fun (nickkey,_) p -> p ++ str " " ++ str nickkey ++ fnl ()) !ref_table (mt ()) ++ fnl () - - - diff --git a/library/goptions.mli b/library/goptions.mli index 900217e06b..b91553bf3c 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -131,6 +131,9 @@ val declare_string_option: ?preprocess:(string -> string) -> val declare_stringopt_option: ?preprocess:(string option -> string option) -> string option option_sig -> unit +(** Helper to declare a reference controlled by an option. Read-only + as to avoid races. *) +val declare_bool_option_and_ref : depr:bool -> name:string -> key:option_name -> value:bool -> (unit -> bool) (** {6 Special functions supposed to be used only in vernacentries.ml } *) diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index b48030b963..c9221ef758 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -576,6 +576,8 @@ END { +type ssrfwdview = ast_closure_term list + let pr_ssrfwdview _ _ _ = pr_view2 } @@ -637,6 +639,7 @@ let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v) | IPatTac _ -> assert false (*internal usage only *) +type ssripatrep = ssripat let wit_ssripatrep = add_genarg "ssripatrep" pr_ipat let pr_ssripat _ _ _ = pr_ipat @@ -1933,6 +1936,7 @@ END (* argument *) { +type ssreqid = ssripatrep option let pr_eqid = function Some pat -> str " " ++ pr_ipat pat | None -> mt () let pr_ssreqid _ _ _ = pr_eqid @@ -1987,10 +1991,12 @@ END (* the entry point parses only non-empty arguments to avoid conflicts *) (* with the basic Coq tactics. *) -(* type ssrarg = ssrbwdview * (ssreqid * (ssrdgens * ssripats)) *) - { +type ssrarg = ssrfwdview * (ssreqid * (cpattern ssragens * ssripats)) + +(* type ssrarg = ssrbwdview * (ssreqid * (ssrdgens * ssripats)) *) + let pr_ssrarg _ _ _ (view, (eqid, (dgens, ipats))) = let pri = pr_intros (gens_sep dgens) in pr_view2 view ++ pr_eqid eqid ++ pr_dgens pr_gen dgens ++ pri ipats diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index 862a93765d..a2cbd3c9c8 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -28,10 +28,22 @@ open Ssrmatching open Ssrast open Ssrequality +type ssrfwdview = ast_closure_term list +type ssreqid = ssripat option +type ssrarg = ssrfwdview * (ssreqid * (cpattern ssragens * ssripats)) + +val wit_ssripatrep : ssripat Genarg.uniform_genarg_type +val wit_ssrarg : ssrarg Genarg.uniform_genarg_type val wit_ssrrwargs : ssrrwarg list Genarg.uniform_genarg_type val wit_ssrclauses : clauses Genarg.uniform_genarg_type val wit_ssrcasearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type val wit_ssrmovearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type val wit_ssrapplyarg : ssrapplyarg Genarg.uniform_genarg_type val wit_ssrhavefwdwbinders : - (Tacexpr.raw_tactic_expr fwdbinders, Tacexpr.glob_tactic_expr fwdbinders, Tacinterp.Value.t fwdbinders) Genarg.genarg_type + (Tacexpr.raw_tactic_expr fwdbinders, + Tacexpr.glob_tactic_expr fwdbinders, + Tacinterp.Value.t fwdbinders) Genarg.genarg_type +val wit_ssrhintarg : + (Tacexpr.raw_tactic_expr ssrhint, + Tacexpr.glob_tactic_expr ssrhint, + Tacinterp.Value.t ssrhint) Genarg.genarg_type diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 7104b8586e..f8289f558c 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -183,14 +183,11 @@ let cofixp_reducible flgs _ stk = else false -let debug_cbv = ref false -let () = Goptions.(declare_bool_option { - optdepr = false; - optname = "cbv visited constants display"; - optkey = ["Debug";"Cbv"]; - optread = (fun () -> !debug_cbv); - optwrite = (fun a -> debug_cbv:=a); -}) +let get_debug_cbv = Goptions.declare_bool_option_and_ref + ~depr:false + ~value:false + ~name:"cbv visited constants display" + ~key:["Debug";"Cbv"] let debug_pr_key = function | ConstKey (sp,_) -> Names.Constant.print sp @@ -325,14 +322,14 @@ and norm_head_ref k info env stack normt = if red_set_ref info.reds normt then match cbv_value_cache info normt with | Some body -> - if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt); + if get_debug_cbv () then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt); strip_appl (shift_value k body) stack | None -> - if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); + if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); (VAL(0,make_constr_ref k normt),stack) else begin - if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); + if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); (VAL(0,make_constr_ref k normt),stack) end diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 1edcc499f0..f18040accb 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -398,16 +398,12 @@ let class_params = function let add_class cl = add_new_class cl { cl_param = class_params cl } -let automatically_import_coercions = ref false - -open Goptions -let () = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "automatic import of coercions"; - optkey = ["Automatic";"Coercions";"Import"]; - optread = (fun () -> !automatically_import_coercions); - optwrite = (:=) automatically_import_coercions } +let get_automatically_import_coercions = + Goptions.declare_bool_option_and_ref + ~depr:true (* Remove in 8.8 *) + ~name:"automatic import of coercions" + ~key:["Automatic";"Coercions";"Import"] + ~value:false let cache_coercion (_, c) = let () = add_class c.coercion_source in @@ -425,7 +421,7 @@ let cache_coercion (_, c) = add_coercion_in_graph (xf,is,it) let load_coercion _ o = - if !automatically_import_coercions then + if get_automatically_import_coercions () then cache_coercion o let set_coercion_in_scope (_, c) = @@ -435,7 +431,7 @@ let set_coercion_in_scope (_, c) = let open_coercion i o = if Int.equal i 1 then begin set_coercion_in_scope o; - if not !automatically_import_coercions then + if not (get_automatically_import_coercions ()) then cache_coercion o end diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 30eb70d0e7..4d1d405bd7 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -33,16 +33,12 @@ open Evd open Termops open Globnames -let use_typeclasses_for_conversion = ref true - -let () = - Goptions.(declare_bool_option - { optdepr = false; - optname = "use typeclass resolution during conversion"; - optkey = ["Typeclass"; "Resolution"; "For"; "Conversion"]; - optread = (fun () -> !use_typeclasses_for_conversion); - optwrite = (fun b -> use_typeclasses_for_conversion := b) } - ) +let get_use_typeclasses_for_conversion = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"use typeclass resolution during conversion" + ~key:["Typeclass"; "Resolution"; "For"; "Conversion"] + ~value:true (* Typing operations dealing with coercions *) exception NoCoercion @@ -424,7 +420,7 @@ let inh_app_fun resolve_tc env evd j = try inh_app_fun_core env evd j with | NoCoercion when not resolve_tc - || not !use_typeclasses_for_conversion -> (evd, j) + || not (get_use_typeclasses_for_conversion ()) -> (evd, j) | NoCoercion -> try inh_app_fun_core env (saturate_evd env evd) j with NoCoercion -> (evd, j) @@ -534,7 +530,7 @@ let inh_conv_coerce_to_gen ?loc resolve_tc rigidonly env evd cj t = coerce_itf ?loc env evd (Some cj.uj_val) cj.uj_type t else raise NoSubtacCoercion with - | NoSubtacCoercion when not resolve_tc || not !use_typeclasses_for_conversion -> + | NoSubtacCoercion when not resolve_tc || not (get_use_typeclasses_for_conversion ()) -> error_actual_type ?loc env best_failed_evd cj t e | NoSubtacCoercion -> let evd' = saturate_evd env evd in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 3391750209..f5e48bcd39 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -105,16 +105,12 @@ let search_guard ?loc env possible_indexes fixdefs = (* To force universe name declaration before use *) -let strict_universe_declarations = ref true -let is_strict_universe_declarations () = !strict_universe_declarations - -let () = - Goptions.(declare_bool_option - { optdepr = false; - optname = "strict universe declaration"; - optkey = ["Strict";"Universe";"Declaration"]; - optread = is_strict_universe_declarations; - optwrite = (:=) strict_universe_declarations }) +let is_strict_universe_declarations = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"strict universe declaration" + ~key:["Strict";"Universe";"Declaration"] + ~value:true (** Miscellaneous interpretation functions *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index c68890a87f..d732544c5c 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -31,19 +31,12 @@ type 'a hint_info_gen = type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen -let typeclasses_unique_solutions = ref false -let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d -let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions - -open Goptions - -let () = - declare_bool_option - { optdepr = false; - optname = "check that typeclasses proof search returns unique solutions"; - optkey = ["Typeclasses";"Unique";"Solutions"]; - optread = get_typeclasses_unique_solutions; - optwrite = set_typeclasses_unique_solutions; } +let get_typeclasses_unique_solutions = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"check that typeclasses proof search returns unique solutions" + ~key:["Typeclasses";"Unique";"Solutions"] + ~value:false let (add_instance_hint, add_instance_hint_hook) = Hook.make () let add_instance_hint id = Hook.get add_instance_hint id @@ -434,28 +427,40 @@ let remove_instance i = Lib.add_anonymous_leaf (instance_input (RemoveInstance, i)); remove_instance_hint i.is_impl -let declare_instance info local glob = +let warning_not_a_class = + let name = "not-a-class" in + let category = "typeclasses" in + CWarnings.create ~name ~category (fun (n, ty) -> + let env = Global.env () in + let evd = Evd.from_env env in + Pp.(str "Ignored instance declaration for “" + ++ Nametab.pr_global_env Id.Set.empty n + ++ str "”: “" + ++ Termops.Internal.print_constr_env env evd (EConstr.of_constr ty) + ++ str "” is not a class") + ) + +let declare_instance ?(warn = false) info local glob = let ty, _ = Typeops.type_of_global_in_context (Global.env ()) glob in let info = Option.default {hint_priority = None; hint_pattern = None} info in match class_of_constr Evd.empty (EConstr.of_constr ty) with | Some (rels, ((tc,_), args) as _cl) -> assert (not (isVarRef glob) || local); add_instance (new_instance tc info (not local) glob) - | None -> () + | None -> if warn then warning_not_a_class (glob, ty) let add_class cl = add_class cl; List.iter (fun (n, inst, body) -> - match inst with - | Some (Backward, info) -> - (match body with - | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance") - | Some b -> declare_instance (Some info) false (ConstRef b)) - | _ -> ()) - cl.cl_projs + match inst with + | Some (Backward, info) -> + (match body with + | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance") + | Some b -> declare_instance ~warn:true (Some info) false (ConstRef b)) + | _ -> ()) + cl.cl_projs - (* * interface functions *) diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 8bdac0a575..d00195678b 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -133,7 +133,10 @@ val remove_instance_hint : GlobRef.t -> unit val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t -val declare_instance : hint_info option -> bool -> GlobRef.t -> unit +(** Declares the given global reference as an instance of its type. + Does nothing — or emit a “not-a-class” warning if the [warn] argument is set — + when said type is not a registered type class. *) +val declare_instance : ?warn:bool -> hint_info option -> bool -> GlobRef.t -> unit (** Build the subinstances hints for a given typeclass object. diff --git a/stm/stm.ml b/stm/stm.ml index a74a67c935..94405924b7 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -44,7 +44,6 @@ module AsyncOpts = struct async_proofs_mode : async_proofs; async_proofs_private_flags : string option; - async_proofs_full : bool; async_proofs_never_reopen_branch : bool; async_proofs_tac_error_resilience : tac_error_filter; @@ -61,7 +60,6 @@ module AsyncOpts = struct async_proofs_mode = APoff; async_proofs_private_flags = None; - async_proofs_full = false; async_proofs_never_reopen_branch = false; async_proofs_tac_error_resilience = `Only [ "curly" ]; @@ -1442,11 +1440,14 @@ end = struct (* {{{ *) let perspective = ref [] let set_perspective l = perspective := l + let is_inside_perspective st = true + (* This code is now disabled. If an IDE needs this feature, make it accessible again. + List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) st + *) + let task_match age t = match age, t with - | Fresh, BuildProof { t_states } -> - not !cur_opt.async_proofs_full || - List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) t_states + | Fresh, BuildProof { t_states } -> is_inside_perspective t_states | Old my_states, States l -> List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l | _ -> false @@ -1482,8 +1483,7 @@ end = struct (* {{{ *) feedback (InProgress ~-1); t_assign (`Val pl); record_pb_time ?loc:t_loc t_name time; - if !cur_opt.async_proofs_full || t_drop - then `Stay(t_states,[States t_states]) + if t_drop then `Stay(t_states,[States t_states]) else `End | Fresh, BuildProof { t_assign; t_loc; t_name; t_states }, RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } -> @@ -2126,8 +2126,7 @@ end = struct (* {{{ *) TaskQueue.enqueue_task (Option.get !queue) QueryTask.({ t_where = prev; t_for = id; t_what = q }) ~cancel_switch - let init () = queue := Some (TaskQueue.create - (if !cur_opt.async_proofs_full then 1 else 0)) + let init () = queue := Some (TaskQueue.create 0) end (* }}} *) @@ -2150,7 +2149,6 @@ let async_policy () = let delegate name = get_hint_bp_time name >= !cur_opt.async_proofs_delegation_threshold || VCS.is_vio_doc () - || !cur_opt.async_proofs_full let collect_proof keep cur hd brkind id = stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); @@ -2257,8 +2255,7 @@ let collect_proof keep cur hd brkind id = else let rc = collect (Some cur) [] id in if is_empty rc then make_sync `AlreadyEvaluated rc - else if (is_vtkeep keep) && - (not(State.is_cached_and_valid id) || !cur_opt.async_proofs_full) + else if (is_vtkeep keep) && (not(State.is_cached_and_valid id)) then check_policy rc else make_sync `AlreadyEvaluated rc @@ -2646,13 +2643,14 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = name by looking at the load path! *) List.iter Mltop.add_coq_path iload_path; + Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff; + begin match doc_type with | Interactive ln -> let dp = match ln with | TopLogical dp -> dp | TopPhysical f -> dirpath_of_file f in - Safe_typing.allow_delayed_constants := true; Declaremods.start_library dp | VoDoc f -> @@ -2663,7 +2661,6 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = set_compilation_hints f | VioDoc f -> - Safe_typing.allow_delayed_constants := true; let ldir = dirpath_of_file f in check_coq_overwriting ldir; let () = Flags.verbosely Declaremods.start_library ldir in @@ -2841,13 +2838,12 @@ let process_back_meta_command ~newtip ~head oid aast w = VCS.commit id (Alias (oid,aast)); Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok -let allow_nested_proofs = ref false -let () = Goptions.(declare_bool_option - { optdepr = false; - optname = "Nested Proofs Allowed"; - optkey = Vernac_classifier.stm_allow_nested_proofs_option_name; - optread = (fun () -> !allow_nested_proofs); - optwrite = (fun b -> allow_nested_proofs := b) }) +let get_allow_nested_proofs = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"Nested Proofs Allowed" + ~key:Vernac_classifier.stm_allow_nested_proofs_option_name + ~value:false let process_transaction ~doc ?(newtip=Stateid.fresh ()) ({ verbose; loc; expr } as x) c = @@ -2869,11 +2865,10 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) | VtQuery, w -> let id = VCS.new_node ~id:newtip () in let queue = - if !cur_opt.async_proofs_full then `QueryQueue (ref false) - else if VCS.is_vio_doc () && - VCS.((get_branch head).kind = `Master) && - may_pierce_opaque (Vernacprop.under_control x.expr) - then `SkipQueue + if VCS.is_vio_doc () && + VCS.((get_branch head).kind = `Master) && + may_pierce_opaque (Vernacprop.under_control x.expr) + then `SkipQueue else `MainQueue in VCS.commit id (mkTransCmd x [] false queue); Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok @@ -2881,7 +2876,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) (* Proof *) | VtStartProof (mode, guarantee, names), w -> - if not !allow_nested_proofs && VCS.proof_nesting () > 0 then + if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on." |> Pp.str |> (fun s -> (UserError (None, s), Exninfo.null)) @@ -3206,8 +3201,7 @@ let edit_at ~doc id = VCS.delete_boxes_of id; VCS.gc (); VCS.print (); - if not !cur_opt.async_proofs_full then - Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; + Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; VCS.checkout_shallowest_proof_branch (); `NewTip in try diff --git a/stm/stm.mli b/stm/stm.mli index 0c0e19ce5c..b6071fa56b 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -16,7 +16,9 @@ open Names module AsyncOpts : sig type cache = Force - type async_proofs = APoff | APonLazy | APon + type async_proofs = APoff + | APonLazy (* Delays proof checking, but does it in master *) + | APon type tac_error_filter = [ `None | `Only of string list | `All ] type stm_opt = { @@ -27,7 +29,6 @@ module AsyncOpts : sig async_proofs_mode : async_proofs; async_proofs_private_flags : string option; - async_proofs_full : bool; async_proofs_never_reopen_branch : bool; async_proofs_tac_error_resilience : tac_error_filter; diff --git a/test-suite/bugs/closed/bug_8364.v b/test-suite/bugs/closed/bug_8364.v new file mode 100644 index 0000000000..10f955b41f --- /dev/null +++ b/test-suite/bugs/closed/bug_8364.v @@ -0,0 +1,17 @@ +Unset Primitive Projections. + +Record Box (A:Type) := box { unbox : A }. +Arguments box {_} _. Arguments unbox {_} _. + +Definition map {A B} (f:A -> B) x := + match x with box x => box (f x) end. + +Definition tuple (l : Box Type) : Type := + match l with + | box x => x + end. + +Fail Inductive stack : Type -> Type := +| Stack T foos : + tuple (map stack foos) -> + stack T. diff --git a/test-suite/bugs/closed/bug_9014.v b/test-suite/bugs/closed/bug_9014.v new file mode 100644 index 0000000000..c1fdd04a65 --- /dev/null +++ b/test-suite/bugs/closed/bug_9014.v @@ -0,0 +1,19 @@ +(* A type, not a class *) +Variant T := mkT. + +(* In records, :> declares a coercion *) +Record R := { t_of_r :> T }. +Check forall r : R, r = r :> T. + +(* A class *) +Class A := { p : Prop }. +(* A sub-class *) +Class B := { a_of_b :> A ; t_of_b :> T }. +(* The sub-instance is automatically inferred due to :> for a_of_b *) +Check forall b : B, p. +(* No coercion is introduced by :> in t_of_b *) +Fail Check forall b : B, b = b :> T. + +(* Using :> when the RHS is not a class produces a “not-a-class” warning. *) +Set Warnings "+not-a-class". +Fail Class B' := { a_of_b' :> A ; t_of_b' :> T }. diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v index d2116d2183..95daa1bb0c 100644 --- a/test-suite/modules/Nat.v +++ b/test-suite/modules/Nat.v @@ -2,7 +2,7 @@ Definition T := nat. Definition le := le. -Hint Unfold le. +Hint Unfold le : core. Lemma le_refl : forall n : nat, le n n. auto. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 60c64d306b..1fb0a37e16 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -77,7 +77,7 @@ End CompareFacts. (** * Properties of [OrderedTypeFull] *) -Module Type OrderedTypeFullFacts (Import O:OrderedTypeFull'). +Module OrderedTypeFullFacts (Import O:OrderedTypeFull'). Module OrderTac := OTF_to_OrderTac O. Ltac order := OrderTac.order. diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index fb6d07d6cf..b248b87880 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -119,7 +119,8 @@ let compile opts ~echo ~f_in ~f_out = Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); let wall_clock1 = Unix.gettimeofday () in - let state = Vernac.load_vernac ~echo ~check:true ~interactive:false ~state long_f_dot_v in + let check = Stm.AsyncOpts.(stm_options.async_proofs_mode = APoff) in + let state = Vernac.load_vernac ~echo ~check ~interactive:false ~state long_f_dot_v in let _doc = Stm.join ~doc:state.doc in let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); @@ -148,6 +149,8 @@ let compile opts ~echo ~f_in ~f_out = document anyways. *) let stm_options = let open Stm.AsyncOpts in { stm_options with + async_proofs_mode = APon; + async_proofs_n_workers = 0; async_proofs_cmd_error_resilience = false; async_proofs_tac_error_resilience = `None; } in diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 2f84eb9851..6c4ea9afa1 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -91,7 +91,7 @@ type coq_cmdopts = { let default_toplevel = Names.(DirPath.make [Id.of_string "Top"]) -let init_args = { +let default_opts = { load_init = true; load_rcfile = true; @@ -139,6 +139,8 @@ let init_args = { print_emacs = false; + (* Quiet / verbosity options should be here *) + inputstate = None; outputstate = None; } @@ -166,6 +168,7 @@ let add_compat_require opts v = | Flags.Current -> add_vo_require opts "Coq.Compat.Coq89" None (Some false) let set_batch_mode opts = + (* XXX: This should be in the argument record *) Flags.quiet := true; System.trust_file_cache := true; { opts with batch_mode = true } @@ -281,11 +284,6 @@ let get_cache opt = function | "force" -> Some Stm.AsyncOpts.Force | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 -let get_identifier opt s = - try Names.Id.of_string s - with CErrors.UserError _ -> - prerr_endline ("Error: valid identifier expected after option "^opt); exit 1 - let is_not_dash_option = function | Some f when String.length f > 0 && f.[0] <> '-' -> true | _ -> false @@ -325,7 +323,7 @@ let usage batch = else Usage.print_usage_coqtop () (* Main parsing routine *) -let parse_args arglist : coq_cmdopts * string list = +let parse_args init_opts arglist : coq_cmdopts * string list = let args = ref arglist in let extras = ref [] in let rec parse oval = match !args with @@ -478,7 +476,9 @@ let parse_args arglist : coq_cmdopts * string list = add_load_vernacular oval true (next ()) |"-mangle-names" -> - Namegen.set_mangle_names_mode (get_identifier opt (next ())); oval + Goptions.set_bool_option_value ["Mangle"; "Names"] true; + Goptions.set_string_option_value ["Mangle"; "Names"; "Prefix"] (next ()); + oval |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 @@ -543,10 +543,6 @@ let parse_args arglist : coq_cmdopts * string list = (* Options with zero arg *) |"-async-queries-always-delegate" |"-async-proofs-always-delegate" - |"-async-proofs-full" -> - { oval with stm_flags = { oval.stm_flags with - Stm.AsyncOpts.async_proofs_full = true; - }} |"-async-proofs-never-reopen-branch" -> { oval with stm_flags = { oval.stm_flags with Stm.AsyncOpts.async_proofs_never_reopen_branch = true @@ -600,7 +596,7 @@ let parse_args arglist : coq_cmdopts * string list = parse noval in try - parse init_args + parse init_opts with any -> fatal_error any (******************************************************************************) diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index 30f1caab12..e645b0c126 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -63,12 +63,17 @@ type coq_cmdopts = { print_emacs : bool; + (* Quiet / verbosity options should be here *) + inputstate : string option; outputstate : string option; } -val parse_args : string list -> coq_cmdopts * string list +(* Default options *) +val default_opts : coq_cmdopts + +val parse_args : coq_cmdopts -> string list -> coq_cmdopts * string list val exitcode : coq_cmdopts -> int val require_libs : coq_cmdopts -> (string * string option * bool option) list diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index faacbe4c80..edef741ca6 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -148,7 +148,7 @@ let init_gc () = Gc.space_overhead = 120} (** Main init routine *) -let init_toplevel custom_init arglist = +let init_toplevel init_opts custom_init arglist = (* Coq's init process, phase 1: OCaml parameters, basic structures, and IO *) @@ -164,7 +164,7 @@ let init_toplevel custom_init arglist = *) let res = begin try - let opts,extras = parse_args arglist in + let opts,extras = parse_args init_opts arglist in memory_stat := opts.memory_stat; (* If we have been spawned by the Spawn module, this has to be done @@ -252,20 +252,25 @@ let init_toplevel custom_init arglist = Feedback.del_feeder init_feeder; res -type custom_toplevel = { - init : opts:coq_cmdopts -> string list -> coq_cmdopts * string list; - run : opts:coq_cmdopts -> state:Vernac.State.t -> unit; -} +type custom_toplevel = + { init : opts:coq_cmdopts -> string list -> coq_cmdopts * string list + ; run : opts:coq_cmdopts -> state:Vernac.State.t -> unit + ; opts : Coqargs.coq_cmdopts + } let coqtop_init ~opts extra = init_color opts; CoqworkmgrApi.(init !async_proofs_worker_priority); opts, extra -let coqtop_toplevel = { init = coqtop_init; run = Coqloop.loop; } +let coqtop_toplevel = + { init = coqtop_init + ; run = Coqloop.loop + ; opts = Coqargs.default_opts + } let start_coq custom = - match init_toplevel custom.init (List.tl (Array.to_list Sys.argv)) with + match init_toplevel custom.opts custom.init (List.tl (Array.to_list Sys.argv)) with (* Batch mode *) | Some state, opts when not opts.batch_mode -> custom.run ~opts ~state; diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 641448f10a..c95d0aca55 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -12,10 +12,13 @@ [init] is used to do custom command line argument parsing. [run] launches a custom toplevel. *) -type custom_toplevel = { - init : opts:Coqargs.coq_cmdopts -> string list -> Coqargs.coq_cmdopts * string list; - run : opts:Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit; -} +open Coqargs + +type custom_toplevel = + { init : opts:coq_cmdopts -> string list -> coq_cmdopts * string list + ; run : opts:coq_cmdopts -> state:Vernac.State.t -> unit + ; opts : Coqargs.coq_cmdopts + } val coqtop_toplevel : custom_toplevel diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index ee6d5e8843..e4e9a87365 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -23,6 +23,7 @@ let arg_init init ~opts extra_args = let start ~init ~loop = let open Coqtop in let custom = { + opts = Coqargs.default_opts; init = arg_init init; run = (fun ~opts:_ ~state:_ -> loop ()); } in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index cbb77057bd..4926b8c3e1 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -337,32 +337,20 @@ let assumption_message = Declare.assumption_message let default_tactic = ref (Proofview.tclUNIT ()) (* true = hide obligations *) -let hide_obligations = ref false - -let set_hide_obligations = (:=) hide_obligations -let get_hide_obligations () = !hide_obligations - -open Goptions -let () = - declare_bool_option - { optdepr = false; - optname = "Hiding of Program obligations"; - optkey = ["Hide";"Obligations"]; - optread = get_hide_obligations; - optwrite = set_hide_obligations; } - -let shrink_obligations = ref true - -let set_shrink_obligations = (:=) shrink_obligations -let get_shrink_obligations () = !shrink_obligations - -let () = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "Shrinking of Program obligations"; - optkey = ["Shrink";"Obligations"]; - optread = get_shrink_obligations; - optwrite = set_shrink_obligations; } +let get_hide_obligations = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"Hidding of Program obligations" + ~key:["Hide";"Obligations"] + ~value:false + + +let get_shrink_obligations = + Goptions.declare_bool_option_and_ref + ~depr:true (* remove in 8.8 *) + ~name:"Shrinking of Program obligations" + ~key:["Shrink";"Obligations"] + ~value:true let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type) diff --git a/vernac/record.ml b/vernac/record.ml index 81b33c2e11..f6dbcb5291 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -458,7 +458,7 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class finite def cum ubinders univs id idbuild paramimpls params arity +let declare_class def cum ubinders univs id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) coers priorities = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) @@ -671,7 +671,7 @@ let definition_structure udecl kind ~template cum poly finite records = in let priorities = List.map (fun ((_, id), _) -> {hint_priority = id; hint_pattern = None}) cfs in let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in - declare_class finite def cum ubinders univs id.CAst.v idbuild + declare_class def cum ubinders univs id.CAst.v idbuild implpars params arity template implfs fields coers priorities | _ -> let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index fa1082473e..a157e01fc1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -582,10 +582,15 @@ let should_treat_as_cumulative cum poly = else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") | None -> poly && Flags.is_polymorphic_inductive_cumulativity () -let uniform_inductive_parameters = ref false +let get_uniform_inductive_parameters = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"Uniform inductive parameters" + ~key:["Uniform"; "Inductive"; "Parameters"] + ~value:false let should_treat_as_uniform () = - if !uniform_inductive_parameters + if get_uniform_inductive_parameters () then ComInductive.UniformParameters else ComInductive.NonUniformParameters @@ -1538,14 +1543,6 @@ let () = optwrite = Flags.make_polymorphic_inductive_cumulativity } let () = - declare_bool_option - { optdepr = false; - optname = "Uniform inductive parameters"; - optkey = ["Uniform"; "Inductive"; "Parameters"]; - optread = (fun () -> !uniform_inductive_parameters); - optwrite = (fun b -> uniform_inductive_parameters := b) } - -let () = declare_int_option { optdepr = false; optname = "the level of inlining during functor application"; |