diff options
Diffstat (limited to 'vernac')
33 files changed, 226 insertions, 238 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index dacef1cb18..fb61a1089f 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -240,8 +240,16 @@ and traverse_inductive (curr, data, ax2ty) mind obj = (* Build the context of all arities *) let arities_ctx = let global_env = Global.env () in + let instance = + let open Univ in + Instance.of_array + (Array.init + (AUContext.size + (Declareops.inductive_polymorphic_context mib)) + Level.var) + in Array.fold_left (fun accu oib -> - let pspecif = Univ.in_punivs (mib, oib) in + let pspecif = ((mib, oib), instance) in let ind_type = Inductive.type_of_inductive global_env pspecif in let indr = oib.mind_relevance in let ind_name = Name oib.mind_typename in @@ -356,8 +364,5 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu in - if not mind.mind_typing_flags.check_template then - let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in - ContextObjectMap.add (Axiom (TemplatePolymorphic m, l)) Constr.mkProp accu - else accu + accu in GlobRef.Map_env.fold fold graph ContextObjectMap.empty diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 68d2c3a00d..194308b77f 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -154,7 +154,6 @@ let program_mode = ref false let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "use of the program extension"; optkey = program_mode_option_name; optread = (fun () -> !program_mode); optwrite = (fun b -> program_mode:=b) } @@ -188,7 +187,6 @@ let is_universe_polymorphism = let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "universe polymorphism"; optkey = universe_polymorphism_option_name; optread = (fun () -> !b); optwrite = ((:=) b) } diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index f954915cf8..6bdb3159cf 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -395,7 +395,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = in Proofview.Goal.enter begin fun gl -> - let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in + let type_of_pq = Tacmach.New.pf_get_type_of gl p in let sigma = Tacmach.New.project gl in let env = Tacmach.New.pf_env gl in let u,v = destruct_ind env sigma type_of_pq @@ -458,11 +458,11 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = match (l1,l2) with | (t1::q1,t2::q2) -> Proofview.Goal.enter begin fun gl -> - let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in let sigma = Tacmach.New.project gl in let env = Tacmach.New.pf_env gl in if EConstr.eq_constr sigma t1 t2 then aux q1 q2 else ( + let tt1 = Tacmach.New.pf_get_type_of gl t1 in let u,v = try destruct_ind env sigma tt1 (* trick so that the good sequence is returned*) with e when CErrors.noncritical e -> indu,[||] diff --git a/vernac/classes.ml b/vernac/classes.ml index c9b5144299..b92c9e9b71 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -42,13 +42,10 @@ let () = Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state let add_instance_hint inst path local info poly = - let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) - | IsGlobal gr -> Hints.IsGlobRef gr - in Flags.silently (fun () -> Hints.add_hints ~local [typeclasses_db] (Hints.HintsResolveEntry - [info, poly, false, Hints.PathHints path, inst'])) () + [info, poly, false, Hints.PathHints path, inst])) () let is_local_for_hint i = match i.is_global with @@ -61,9 +58,9 @@ let is_local_for_hint i = let add_instance check inst = let poly = Global.is_polymorphic inst.is_impl in let local = is_local_for_hint inst in - add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] local + add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] local inst.is_info poly; - List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path + List.iter (fun (path, pri, c) -> add_instance_hint (Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)) path local pri poly) (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) @@ -513,7 +510,7 @@ let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri let interp_instance_context ~program_mode env ctx ~generalize pl tclass = let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in let tclass = - if generalize then CAst.make @@ CGeneralization (Glob_term.Implicit, Some AbsPi, tclass) + if generalize then CAst.make @@ CGeneralization (Glob_term.MaxImplicit, Some AbsPi, tclass) else tclass in let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml index 15077298aa..9d43debb77 100644 --- a/vernac/comArguments.ml +++ b/vernac/comArguments.ml @@ -228,7 +228,7 @@ let vernac_arguments ~section_local reference args more_implicits flags = let implicits = List.map (List.map snd) implicits in let implicits_specified = match implicits with - | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l + | [l] -> List.exists (function Glob_term.Explicit -> false | _ -> true) l | _ -> true in if implicits_specified && clear_implicits_flag then diff --git a/vernac/comArguments.mli b/vernac/comArguments.mli index 71effddf67..cbc5fc15e2 100644 --- a/vernac/comArguments.mli +++ b/vernac/comArguments.mli @@ -12,6 +12,6 @@ val vernac_arguments : section_local:bool -> Libnames.qualid Constrexpr.or_by_notation -> Vernacexpr.vernac_argument_status list - -> (Names.Name.t * Impargs.implicit_kind) list list + -> (Names.Name.t * Glob_term.binding_kind) list list -> Vernacexpr.arguments_modifier list -> unit diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 625ffb5a06..d97bf6724c 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -270,7 +270,7 @@ let context ~poly l = | Some (Name id',_) -> Id.equal name id' | _ -> false in - let impl = Glob_term.(if List.exists test impls then Implicit else Explicit) in + let impl = Glob_term.(if List.exists test impls then MaxImplicit else Explicit) in (* ??? *) name,b,t,impl) ctx in diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml index 56ab6f289d..2c582da495 100644 --- a/vernac/comCoercion.ml +++ b/vernac/comCoercion.ml @@ -198,10 +198,9 @@ let build_id_coercion idf_opt source poly = lams in (* juste pour verification *) - let _ = - if not - (Reductionops.is_conv_leq env sigma - (Typing.unsafe_type_of env sigma (EConstr.of_constr val_f)) (EConstr.of_constr typ_f)) + let sigma, val_t = Typing.type_of env sigma (EConstr.of_constr val_f) in + let () = + if not (Reductionops.is_conv_leq env sigma val_t (EConstr.of_constr typ_f)) then user_err (strbrk "Cannot be defined as coercion (maybe a bad number of arguments).") diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 8de1c69424..d711c9aea0 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -42,7 +42,6 @@ let should_auto_template = let auto = ref true in let () = declare_bool_option { optdepr = false; - optname = "Automatically make some inductive types template polymorphic"; optkey = ["Auto";"Template";"Polymorphism"]; optread = (fun () -> !auto); optwrite = (fun b -> auto := b); } @@ -323,16 +322,15 @@ let check_named {CAst.loc;v=na} = match na with let msg = str "Parameters must be named." in user_err ?loc msg -let template_polymorphism_candidate ~template_check ~ctor_levels uctx params concl = +let template_polymorphism_candidate ~ctor_levels uctx params concl = match uctx with | Entries.Monomorphic_entry uctx -> let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in if not concltemplate then false - else if not template_check then true else let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in let params, conclunivs = - IndTyping.template_polymorphic_univs ~template_check ~ctor_levels uctx params conclu + IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu in not (Univ.LSet.is_empty conclunivs) | Entries.Polymorphic_entry _ -> false @@ -385,7 +383,7 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames List.fold_left (fun levels c -> add_levels c levels) param_levels ctypes in - template_polymorphism_candidate ~template_check:(Environ.check_template env_ar_params) ~ctor_levels uctx ctx_params concl + template_polymorphism_candidate ~ctor_levels uctx ctx_params concl in let template = match template with | Some template -> diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index cc104b3762..1286e4a5c3 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -76,17 +76,15 @@ val should_auto_template : Id.t -> bool -> bool inductive under consideration. *) val template_polymorphism_candidate - : template_check:bool - -> ctor_levels:Univ.LSet.t + : ctor_levels:Univ.LSet.t -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool -(** [template_polymorphism_candidate ~template_check ~ctor_levels uctx params +(** [template_polymorphism_candidate ~ctor_levels uctx params conclsort] is [true] iff an inductive with params [params], conclusion [conclsort] and universe levels appearing in the constructor arguments [ctor_levels] would be definable as template polymorphic. It should have at least one universe in its monomorphic universe context that can be made parametric in its - conclusion sort, if one is given. If the [template_check] flag is - false we just check that the conclusion sort is not small. *) + conclusion sort, if one is given. *) diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index d48e2139d1..84f8578ad4 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -127,7 +127,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let binders = letbinders @ [arg] in let binders_env = push_rel_context binders_rel env in let sigma, (rel, _) = interp_constr_evars_impls ~program_mode:true env sigma r in - let relty = Typing.unsafe_type_of env sigma rel in + let relty = Retyping.get_type_of env sigma rel in let relargty = let error () = user_err ?loc:(constr_loc r) diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml index 2375028541..7dd53564cc 100644 --- a/vernac/declareInd.ml +++ b/vernac/declareInd.ml @@ -60,9 +60,9 @@ let cache_inductive ((sp, kn), names) = let discharge_inductive ((sp, kn), names) = Some names -let inInductive : inductive_obj -> Libobject.obj = +let objInductive : inductive_obj Libobject.Dyn.tag = let open Libobject in - declare_object {(default_object "INDUCTIVE") with + declare_object_full {(default_object "INDUCTIVE") with cache_function = cache_inductive; load_function = load_inductive; open_function = open_inductive; @@ -71,6 +71,7 @@ let inInductive : inductive_obj -> Libobject.obj = discharge_function = discharge_inductive; } +let inInductive v = Libobject.Dyn.Easy.inj v objInductive let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c @@ -212,3 +213,9 @@ let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie p if mie.mind_entry_private == None then Indschemes.declare_default_schemes mind; mind + +module Internal = +struct + type nonrec inductive_obj = inductive_obj + let objInductive = objInductive +end diff --git a/vernac/declareInd.mli b/vernac/declareInd.mli index df8895a999..17647d50aa 100644 --- a/vernac/declareInd.mli +++ b/vernac/declareInd.mli @@ -21,3 +21,12 @@ val declare_mutual_inductive_with_eliminations -> UnivNames.universe_binders -> one_inductive_impls list -> Names.MutInd.t + +(** {6 For legacy support, do not use} *) +module Internal : +sig + +type inductive_obj +val objInductive : inductive_obj Libobject.Dyn.tag + +end diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index b56b9c8ce2..dcb28b898f 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -56,7 +56,7 @@ type program_info = let get_shrink_obligations = Goptions.declare_bool_option_and_ref ~depr:true (* remove in 8.8 *) - ~name:"Shrinking of Program obligations" ~key:["Shrink"; "Obligations"] + ~key:["Shrink"; "Obligations"] ~value:true (* XXX: Is this the right place for this? *) @@ -133,7 +133,6 @@ let add_hint local prg cst = let get_hide_obligations = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"Hidding of Program obligations" ~key:["Hide"; "Obligations"] ~value:false diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml index 69ba9d76ec..def2fdad2a 100644 --- a/vernac/declareUniv.ml +++ b/vernac/declareUniv.ml @@ -72,7 +72,7 @@ let declare_univ_binders gr pl = CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") | ConstructRef _ -> CErrors.anomaly ~label:"declare_univ_binders" - Pp.(str "declare_univ_binders on an constructor reference") + Pp.(str "declare_univ_binders on a constructor reference") in let univs = Id.Map.fold (fun id univ univs -> match Univ.Level.name univ with diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 3302231fd1..d0374bc4fa 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -16,7 +16,6 @@ open Util open Names open Glob_term open Vernacexpr -open Impargs open Constrexpr open Constrexpr_ops open Extend @@ -817,7 +816,7 @@ GRAMMAR EXTEND Gram { let name, recarg_like, notation_scope = item in [RealArg { name=name; recarg_like=recarg_like; notation_scope=notation_scope; - implicit_status = NotImplicit}] } + implicit_status = Explicit}] } | "/" -> { [VolatileArg] } | "&" -> { [BidiArg] } | "("; items = LIST1 argument_spec; ")"; sc = OPT scope_delimiter -> @@ -827,7 +826,7 @@ GRAMMAR EXTEND Gram List.map (fun (name,recarg_like,notation_scope) -> RealArg { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; - implicit_status = NotImplicit}) items } + implicit_status = Explicit}) items } | "["; items = LIST1 argument_spec; "]"; sc = OPT scope_delimiter -> { let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x @@ -835,7 +834,7 @@ GRAMMAR EXTEND Gram List.map (fun (name,recarg_like,notation_scope) -> RealArg { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; - implicit_status = Implicit}) items } + implicit_status = NonMaxImplicit}) items } | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope_delimiter -> { let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x @@ -843,16 +842,16 @@ GRAMMAR EXTEND Gram List.map (fun (name,recarg_like,notation_scope) -> RealArg { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; - implicit_status = MaximallyImplicit}) items } + implicit_status = MaxImplicit}) items } ] ]; (* Same as [argument_spec_block], but with only implicit status and names *) more_implicits_block: [ - [ name = name -> { [(name.CAst.v, NotImplicit)] } + [ name = name -> { [(name.CAst.v, Explicit)] } | "["; items = LIST1 name; "]" -> - { List.map (fun name -> (name.CAst.v, Impargs.Implicit)) items } + { List.map (fun name -> (name.CAst.v, NonMaxImplicit)) items } | "{"; items = LIST1 name; "}" -> - { List.map (fun name -> (name.CAst.v, MaximallyImplicit)) items } + { List.map (fun name -> (name.CAst.v, MaxImplicit)) items } ] ]; strategy_level: diff --git a/vernac/himsg.ml b/vernac/himsg.ml index ba7ae5069b..dfc4631572 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -201,9 +201,7 @@ let explain_bad_assumption env sigma j = str "because this term is not a type." let explain_reference_variables sigma id c = - (* c is intended to be a global reference *) - let pc = pr_global (fst (Termops.global_of_constr sigma c)) in - pc ++ strbrk " depends on the variable " ++ Id.print id ++ + pr_global c ++ strbrk " depends on the variable " ++ Id.print id ++ strbrk " which is not declared in the context." let rec pr_disjunction pr = function @@ -1216,8 +1214,12 @@ let error_bad_entry () = let error_large_non_prop_inductive_not_in_type () = str "Large non-propositional inductive types must be in Type." -let error_inductive_bad_univs () = - str "Incorrect universe constraints declared for inductive type." +let error_inductive_missing_constraints (us,ind_univ) = + let pr_u = Univ.Universe.pr_with UnivNames.pr_with_global_universes 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)) + (Univ.Universe.Set.elements us)) (* Recursion schemes errors *) @@ -1256,7 +1258,7 @@ let explain_inductive_error = function | BadEntry -> error_bad_entry () | LargeNonPropInductiveNotInType -> error_large_non_prop_inductive_not_in_type () - | BadUnivs -> error_inductive_bad_univs () + | MissingConstraints csts -> error_inductive_missing_constraints csts (* Recursion schemes errors *) @@ -1364,7 +1366,6 @@ let explain_exn_default = function | Sys_error msg -> hov 0 (str "System error: " ++ quote (str msg)) | Out_of_memory -> hov 0 (str "Out of memory.") | Stack_overflow -> hov 0 (str "Stack overflow.") - | Dynlink.Error e -> hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e)) | CErrors.Timeout -> hov 0 (str "Timeout!") | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") (* Otherwise, not handled here *) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 2f0b1062a7..227d2f1554 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -44,7 +44,6 @@ let elim_flag = ref true let () = declare_bool_option { optdepr = false; - optname = "automatic declaration of induction schemes"; optkey = ["Elimination";"Schemes"]; optread = (fun () -> !elim_flag) ; optwrite = (fun b -> elim_flag := b) } @@ -53,7 +52,6 @@ let bifinite_elim_flag = ref false let () = declare_bool_option { optdepr = false; - optname = "automatic declaration of induction schemes for non-recursive types"; optkey = ["Nonrecursive";"Elimination";"Schemes"]; optread = (fun () -> !bifinite_elim_flag) ; optwrite = (fun b -> bifinite_elim_flag := b) } @@ -62,7 +60,6 @@ let case_flag = ref false let () = declare_bool_option { optdepr = false; - optname = "automatic declaration of case analysis schemes"; optkey = ["Case";"Analysis";"Schemes"]; optread = (fun () -> !case_flag) ; optwrite = (fun b -> case_flag := b) } @@ -71,7 +68,6 @@ let eq_flag = ref false let () = declare_bool_option { optdepr = false; - optname = "automatic declaration of boolean equality"; optkey = ["Boolean";"Equality";"Schemes"]; optread = (fun () -> !eq_flag) ; optwrite = (fun b -> eq_flag := b) } @@ -82,7 +78,6 @@ let eq_dec_flag = ref false let () = declare_bool_option { optdepr = false; - optname = "automatic declaration of decidable equality"; optkey = ["Decidable";"Equality";"Schemes"]; optread = (fun () -> !eq_dec_flag) ; optwrite = (fun b -> eq_dec_flag := b) } @@ -91,7 +86,6 @@ let rewriting_flag = ref false let () = declare_bool_option { optdepr = false; - optname ="automatic declaration of rewriting schemes for equality types"; optkey = ["Rewriting";"Schemes"]; optread = (fun () -> !rewriting_flag) ; optwrite = (fun b -> rewriting_flag := b) } diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 865eded545..f7606f4ede 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -268,7 +268,6 @@ let warn_let_as_axiom = let get_keep_admitted_vars = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"keep section variables in admitted proofs" ~key:["Keep"; "Admitted"; "Variables"] ~value:true diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 222e9eb825..0c39aba70a 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -126,7 +126,7 @@ let parse_format ({CAst.loc;v=str} : lstring) = let rec parse_non_format i = let n = nonspaces false 0 i in push_token (make_loc i (i+n-1)) (UnpTerminal (String.sub str i n)) (parse_token 1 (i+n)) - and parse_quoted n i = + and parse_quoted n k i = if i < len then match str.[i] with (* Parse " // " *) | '/' when i+1 < len && str.[i+1] == '/' -> @@ -140,7 +140,7 @@ let parse_format ({CAst.loc;v=str} : lstring) = (parse_token 1 (close_quotation i (i+p+1))) | c -> (* The spaces are real spaces *) - push_white i n (match c with + push_white (i-n-1-k) n (match c with | '[' -> if i+1 < len then match str.[i+1] with (* Parse " [h .. ", *) @@ -177,7 +177,7 @@ let parse_format ({CAst.loc;v=str} : lstring) = push_white (i-n) (n-k) (push_token (make_loc i (i+1)) (UnpTerminal "'") (parse_token 1 (i+1))) (* Parse the beginning of a quoted expression *) | '\'' -> - parse_quoted (n-k) (i+1) + parse_quoted (n-k) k (i+1) (* Otherwise *) | _ -> push_white (i-n) (n-k) (parse_non_format i) @@ -477,6 +477,9 @@ let warn_format_break = (fun () -> strbrk "Discarding format implicitly indicated by multiple spaces in notation because an explicit format modifier is given.") +let has_ldots l = + List.exists (function (_,UnpTerminal s) -> String.equal s (Id.to_string Notation_ops.ldots_var) | _ -> false) l + let rec split_format_at_ldots hd = function | (loc,UnpTerminal s) :: fmt when String.equal s (Id.to_string Notation_ops.ldots_var) -> loc, List.rev hd, fmt | u :: fmt -> @@ -504,11 +507,32 @@ let find_prod_list_loc sfmt fmt = (* A separator; we highlight the separating sequence *) Loc.merge_opt (fst (List.hd sfmt)) (fst (List.last sfmt)) +let is_blank s = + let n = String.length s in + let rec aux i s = i >= n || s.[i] = ' ' && aux (i+1) s in + aux 0 s + +let is_formatting = function + | (_,UnpCut _) -> true + | (_,UnpTerminal s) -> is_blank s + | _ -> false + +let rec is_var_in_recursive_format = function + | (_,UnpTerminal s) when not (is_blank s) -> true + | (loc,UnpBox (b,l)) -> + (match List.filter (fun a -> not (is_formatting a)) l with + | [a] -> is_var_in_recursive_format a + | _ -> error_not_same ?loc ()) + | _ -> false + +let rec check_eq_var_upto_name = function + | (_,UnpTerminal s1), (_,UnpTerminal s2) when not (is_blank s1 && is_blank s2) || s1 = s2 -> () + | (_,UnpBox (b1,l1)), (_,UnpBox (b2,l2)) when b1 = b2 -> List.iter check_eq_var_upto_name (List.combine l1 l2) + | (_,UnpCut b1), (_,UnpCut b2) when b1 = b2 -> () + | _, (loc,_) -> error_not_same ?loc () + let skip_var_in_recursive_format = function - | (_,UnpTerminal s) :: sl (* skip first var *) when not (List.for_all (fun c -> c = " ") (String.explode s)) -> - (* To do, though not so important: check that the names match - the names in the notation *) - sl + | a :: sl when is_var_in_recursive_format a -> a, sl | (loc,_) :: _ -> error_not_same ?loc () | [] -> assert false @@ -516,15 +540,20 @@ let read_recursive_format sl fmt = (* Turn [[UnpTerminal s :: some-list @ UnpTerminal ".." :: same-some-list @ UnpTerminal s' :: rest] *) (* into [(some-list,rest)] *) let get_head fmt = - let sl = skip_var_in_recursive_format fmt in - try split_format_at_ldots [] sl with Exit -> error_not_same ?loc:(fst (List.last (if sl = [] then fmt else sl))) () in + let var,sl = skip_var_in_recursive_format fmt in + try var, split_format_at_ldots [] sl + with Exit -> error_not_same ?loc:(fst (List.last (if sl = [] then fmt else sl))) () in let rec get_tail = function | (loc,a) :: sepfmt, (_,b) :: fmt when (=) a b -> get_tail (sepfmt, fmt) (* FIXME *) | [], tail -> skip_var_in_recursive_format tail | (loc,_) :: _, ([] | (_,UnpTerminal _) :: _)-> error_not_same ?loc () | _, (loc,_)::_ -> error_not_same ?loc () in - let loc, slfmt, fmt = get_head fmt in - slfmt, get_tail (slfmt, fmt) + let var1, (loc, slfmt, fmt) = get_head fmt in + let var2, res = get_tail (slfmt, fmt) in + check_eq_var_upto_name (var1,var2); + (* To do, though not so important: check that the names match + the names in the notation *) + slfmt, res let hunks_of_format (from,(vars,typs)) symfmt = let rec aux = function @@ -537,13 +566,9 @@ let hunks_of_format (from,(vars,typs)) symfmt = | NonTerminal s :: symbs, (_,UnpTerminal s') :: fmt when Id.equal s (Id.of_string s') -> let i = index_id s vars in let symbs, l = aux (symbs,fmt) in symbs, unparsing_metavar i from typs :: l - | symbs, (_,UnpBox (a,b)) :: fmt -> - let symbs', b' = aux (symbs,b) in - let symbs', l = aux (symbs',fmt) in - symbs', UnpBox (a,List.map (fun x -> (None,x)) b') :: l | symbs, (_,(UnpCut _ as u)) :: fmt -> let symbs, l = aux (symbs,fmt) in symbs, u :: l - | SProdList (m,sl) :: symbs, fmt -> + | SProdList (m,sl) :: symbs, fmt when has_ldots fmt -> let i = index_id m vars in let typ = List.nth typs (i-1) in let _,prec = precedence_of_entry_type from typ in @@ -558,6 +583,10 @@ let hunks_of_format (from,(vars,typs)) symfmt = UnpBinderListMetaVar (i,isopen,slfmt) | _ -> assert false in symbs, hunk :: l + | symbs, (_,UnpBox (a,b)) :: fmt -> + let symbs', b' = aux (symbs,b) in + let symbs', l = aux (symbs',fmt) in + symbs', UnpBox (a,List.map (fun x -> (None,x)) b') :: l | symbs, [] -> symbs, [] | Break _ :: symbs, fmt -> warn_format_break (); aux (symbs,fmt) | _, fmt -> error_format ?loc:(fst (List.hd fmt)) () @@ -1346,7 +1375,7 @@ let inNotation : notation_obj -> obj = (**********************************************************************) let with_lib_stk_protection f x = - let fs = Lib.freeze ~marshallable:false in + let fs = Lib.freeze () in try let a = f x in Lib.unfreeze fs; a with reraise -> let reraise = CErrors.push reraise in diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 9c18441d9c..ab9d008659 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -11,7 +11,6 @@ open CErrors open Util open Pp -open Libobject open System (* Code to hook Coq into the ML toplevel -- depends on having the @@ -56,7 +55,6 @@ let keep_copy_mlpath path = (* If there is a toplevel under Coq *) type toplevel = { load_obj : string -> unit; - use_file : string -> unit; add_dir : string -> unit; ml_loop : unit -> unit } @@ -94,43 +92,26 @@ let ocaml_toploop () = | WithTop t -> Printexc.catch t.ml_loop () | _ -> () -(* Try to interpret load_obj's (internal) errors *) -let report_on_load_obj_error exc = - let x = Obj.repr exc in - (* Try an horrible (fragile) hack to report on Symtable dynlink errors *) - (* (we follow ocaml's Printexc.to_string decoding of exceptions) *) - if Obj.is_block x && String.equal (Obj.magic (Obj.field (Obj.field x 0) 0)) "Symtable.Error" - then - let err_block = Obj.field x 1 in - if Int.equal (Obj.tag err_block) 0 then - (* Symtable.Undefined_global of string *) - str "reference to undefined global " ++ - str (Obj.magic (Obj.field err_block 0)) - else str (Printexc.to_string exc) - else str (Printexc.to_string exc) - (* Dynamic loading of .cmo/.cma *) +(* We register errors at least for Dynlink, it is possible to do so Symtable + too, as we do in the bytecode init code. +*) +let _ = CErrors.register_handler (function + | Dynlink.Error e -> + hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e)) + | _ -> + raise CErrors.Unhandled + ) + let ml_load s = - match !load with - | WithTop t -> - (try t.load_obj s; s - with - | e when CErrors.noncritical e -> - let e = CErrors.push e in - match fst e with - | (UserError _ | Failure _ | Not_found as u) -> Exninfo.iraise (u, snd e) - | exc -> - let msg = report_on_load_obj_error exc in - user_err ~hdr:"Mltop.load_object" (str"Cannot link ml-object " ++ - str s ++ str" to Coq code (" ++ msg ++ str ").")) - | WithoutTop -> - try - Dynlink.loadfile s; s - with Dynlink.Error a -> - user_err ~hdr:"Mltop.load_object" - (strbrk "while loading " ++ str s ++ - strbrk ": " ++ str (Dynlink.error_message a)) + (match !load with + | WithTop t -> + t.load_obj s + | WithoutTop -> + Dynlink.loadfile s + ); + s let dir_ml_load s = match !load with @@ -140,17 +121,6 @@ let dir_ml_load s = let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in ml_load gname -(* Dynamic interpretation of .ml *) -let dir_ml_use s = - match !load with - | WithTop t -> t.use_file s - | _ -> - let moreinfo = - if Sys.(backend_type = Native) then " Loading ML code works only in bytecode." - else "" - in - user_err ~hdr:"Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo) - (* Adds a path to the ML paths *) let add_ml_dir s = match !load with @@ -275,7 +245,6 @@ let load_ml_object mname ?path fname= init_ml_object mname; path -let dir_ml_load m = ignore(dir_ml_load m) let add_known_module m = add_known_module m None (* Summary of declared ML Modules *) @@ -334,23 +303,38 @@ let _ = (* Liboject entries of declared ML Modules *) +(* Digest of module used to compile the file *) +type ml_module_digest = + | NoDigest + | AnyDigest of Digest.t (* digest of any used cma / cmxa *) + type ml_module_object = { mlocal : Vernacexpr.locality_flag; - mnames : string list + mnames : (string * ml_module_digest) list } +let add_module_digest m = + try + let file = file_of_name m in + let path, file = System.where_in_path ~warn:false !coq_mlpath_copy file in + m, AnyDigest (Digest.file file) + with + | Not_found -> + m, NoDigest + let cache_ml_objects (_,{mnames=mnames}) = - let iter obj = trigger_ml_object true true true obj in + let iter (obj, _) = trigger_ml_object true true true obj in List.iter iter mnames let load_ml_objects _ (_,{mnames=mnames}) = - let iter obj = trigger_ml_object true false true obj in + let iter (obj, _) = trigger_ml_object true false true obj in List.iter iter mnames let classify_ml_objects ({mlocal=mlocal} as o) = - if mlocal then Dispose else Substitute o + if mlocal then Libobject.Dispose else Libobject.Substitute o -let inMLModule : ml_module_object -> obj = +let inMLModule : ml_module_object -> Libobject.obj = + let open Libobject in declare_object {(default_object "ML-MODULE") with cache_function = cache_ml_objects; @@ -360,6 +344,7 @@ let inMLModule : ml_module_object -> obj = let declare_ml_modules local l = let l = List.map mod_of_name l in + let l = List.map add_module_digest l in Lib.add_anonymous_leaf ~cache_first:false (inMLModule {mlocal=local; mnames=l}) let print_ml_path () = diff --git a/vernac/mltop.mli b/vernac/mltop.mli index 56a28b64b0..271772d7ba 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -14,7 +14,6 @@ record. *) type toplevel = { load_obj : string -> unit; - use_file : string -> unit; add_dir : string -> unit; ml_loop : unit -> unit } @@ -38,12 +37,6 @@ val add_ml_dir : recursive:bool -> string -> unit (** Tests if we can load ML files *) val has_dynlink : bool -(** Dynamic loading of .cmo *) -val dir_ml_load : string -> unit - -(** Dynamic interpretation of .ml *) -val dir_ml_use : string -> unit - (** List of modules linked to the toplevel *) val add_known_module : string -> unit val module_is_known : string -> bool diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index a1bd99c237..82132a1af6 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1076,14 +1076,14 @@ let string_of_definition_object_kind = let open Decls in function let pr_br imp force x = let left,right = match imp with - | Impargs.Implicit -> str "[", str "]" - | Impargs.MaximallyImplicit -> str "{", str "}" - | Impargs.NotImplicit -> if force then str"(",str")" else mt(),mt() + | Glob_term.NonMaxImplicit -> str "[", str "]" + | Glob_term.MaxImplicit -> str "{", str "}" + | Glob_term.Explicit -> if force then str"(",str")" else mt(),mt() in left ++ x ++ right in let get_arguments_like s imp tl = - if s = None && imp = Impargs.NotImplicit then [], tl + if s = None && imp = Glob_term.Explicit then [], tl else let rec fold extra = function | RealArg arg :: tl when diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index b999ce9f3f..32c438c724 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -211,12 +211,10 @@ let pr_template_variables = function let print_polymorphism ref = let poly = Global.is_polymorphic ref in let template_poly = Global.is_template_polymorphic ref in - let template_checked = Global.is_template_checked ref in let template_variables = Global.get_template_polymorphic_variables ref in [ pr_global ref ++ str " is " ++ (if poly then str "universe polymorphic" else if template_poly then - (if not template_checked then str "assumed " else mt()) ++ str "template universe polymorphic " ++ h 0 (pr_template_variables template_variables) else str "not universe polymorphic") ] @@ -260,18 +258,18 @@ let implicit_name_of_pos = function | Constrexpr.ExplByPos (n,k) -> Anonymous let implicit_kind_of_status = function - | None -> Anonymous, NotImplicit - | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then MaximallyImplicit else Implicit + | None -> Anonymous, Glob_term.Explicit + | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then Glob_term.MaxImplicit else Glob_term.NonMaxImplicit let dummy = { - Vernacexpr.implicit_status = NotImplicit; + Vernacexpr.implicit_status = Glob_term.Explicit; name = Anonymous; recarg_like = false; notation_scope = None; } let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} = - name = Anonymous && not recarg_like && notation_scope = None && implicit_status = NotImplicit + name = Anonymous && not recarg_like && notation_scope = None && implicit_status = Glob_term.Explicit let rec main_implicits i renames recargs scopes impls = if renames = [] && recargs = [] && scopes = [] && impls = [] then [] @@ -283,8 +281,8 @@ let rec main_implicits i renames recargs scopes impls = let (name, implicit_status) = match renames, impls with | _, (Some _ as i) :: _ -> implicit_kind_of_status i - | name::_, _ -> (name,NotImplicit) - | [], (None::_ | []) -> (Anonymous, NotImplicit) + | name::_, _ -> (name,Glob_term.Explicit) + | [], (None::_ | []) -> (Anonymous, Glob_term.Explicit) in let notation_scope = match scopes with | scope :: _ -> Option.map CAst.make scope @@ -670,25 +668,35 @@ let gallina_print_syntactic_def env kn = Constrextern.without_specific_symbols [Notation.SynDefRule kn] (pr_glob_constr_env env) c) -let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) = +module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> Pp.t option end) + +let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with +| f -> f o +| exception Not_found -> None + +(* TODO: this kind of feature should not rely on the Libobject stack. There is + no reason that an object in the stack corresponds to a user-facing + declaration. It may have been so at the time this was written, but this + needs to be done in a more principled way. *) +let gallina_print_leaf_entry env sigma with_values ((sp, kn),lobj) = let sep = if with_values then " = " else " : " in match lobj with | AtomicObject o -> - let tag = object_tag o in - begin match (oname,tag) with - | (_,"VARIABLE") -> + let handler = + DynHandle.add Declare.Internal.objVariable begin fun _ -> (* Outside sections, VARIABLES still exist but only with universes constraints *) (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None) - | (_,"CONSTANT") -> + end @@ + DynHandle.add Declare.Internal.objConstant begin fun _ -> Some (print_constant with_values sep (Constant.make1 kn) None) - | (_,"INDUCTIVE") -> + end @@ + DynHandle.add DeclareInd.Internal.objInductive begin fun _ -> Some (gallina_print_inductive (MutInd.make1 kn) None) - | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| - "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None - (* To deal with forgotten cases... *) - | (_,s) -> None - end + end @@ + DynHandle.empty + in + handle handler o | ModuleObject _ -> let (mp,l) = KerName.repr kn in Some (print_module with_values ~mod_ops:Declaremods.mod_ops (MPdot (mp,l))) @@ -777,11 +785,18 @@ let print_full_context env sigma = let print_full_context_typ env sigma = print_context env sigma false None (Lib.contents ()) +module DynHandleF = Libobject.Dyn.Map(struct type 'a t = 'a -> Pp.t end) + +let handleF h (Libobject.Dyn.Dyn (tag, o)) = match DynHandleF.find tag h with +| f -> f o +| exception Not_found -> mt () + +(* TODO: see the comment for {!gallina_print_leaf_entry} *) let print_full_pure_context env sigma = let rec prec = function | ((_,kn),Lib.Leaf AtomicObject lobj)::rest -> - let pp = match object_tag lobj with - | "CONSTANT" -> + let handler = + DynHandleF.add Declare.Internal.objConstant begin fun _ -> let con = Global.constant_of_delta_kn kn in let cb = Global.lookup_constant con in let typ = cb.const_type in @@ -804,12 +819,16 @@ let print_full_pure_context env sigma = str "Primitive " ++ print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ) ++ str "." ++ fnl () ++ fnl () - | "INDUCTIVE" -> + end @@ + DynHandleF.add DeclareInd.Internal.objInductive begin fun _ -> let mind = Global.mind_of_delta_kn kn in let mib = Global.lookup_mind mind in pr_mutual_inductive_body (Global.env()) mind mib None ++ str "." ++ fnl () ++ fnl () - | _ -> mt () in + end @@ + DynHandleF.empty + in + let pp = handleF handler lobj in prec rest ++ pp | ((_,kn),Lib.Leaf ModuleObject _)::rest -> (* TODO: make it reparsable *) diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index cfb3248c7b..b329463cb0 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -140,7 +140,6 @@ let suggest_proof_using = ref false let () = Goptions.(declare_bool_option { optdepr = false; - optname = "suggest Proof using"; optkey = ["Suggest";"Proof";"Using"]; optread = (fun () -> !suggest_proof_using); optwrite = ((:=) suggest_proof_using) }) @@ -176,7 +175,6 @@ let proof_using_opt_name = ["Default";"Proof";"Using"] let () = Goptions.(declare_stringopt_option { optdepr = false; - optname = "default value for Proof using"; optkey = proof_using_opt_name; optread = (fun () -> Option.map using_to_string !value); optwrite = (fun b -> value := Option.map using_from_string b); diff --git a/vernac/record.ml b/vernac/record.ml index df9b4a0914..27bd390714 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -39,7 +39,6 @@ let primitive_flag = ref false let () = declare_bool_option { optdepr = false; - optname = "use of primitive projections"; optkey = ["Primitive";"Projections"]; optread = (fun () -> !primitive_flag) ; optwrite = (fun b -> primitive_flag := b) } @@ -48,7 +47,6 @@ let typeclasses_strict = ref false let () = declare_bool_option { optdepr = false; - optname = "strict typeclass resolution"; optkey = ["Typeclasses";"Strict";"Resolution"]; optread = (fun () -> !typeclasses_strict); optwrite = (fun b -> typeclasses_strict := b); } @@ -57,7 +55,6 @@ let typeclasses_unique = ref false let () = declare_bool_option { optdepr = false; - optname = "unique typeclass instances"; optkey = ["Typeclasses";"Unique";"Instances"]; optread = (fun () -> !typeclasses_unique); optwrite = (fun b -> typeclasses_unique := b); } @@ -446,8 +443,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa univs) param_levels fields in - let template_check = Environ.check_template (Global.env ()) in - ComInductive.template_polymorphism_candidate ~template_check ~ctor_levels univs params + ComInductive.template_polymorphism_candidate ~ctor_levels univs params (Some (Sorts.sort_of_univ min_univ)) in match template with diff --git a/vernac/search.ml b/vernac/search.ml index 364dae7152..b8825c3b29 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -71,6 +71,14 @@ let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> env -> constr -> unit) = let pfctxt = named_context e in iter_named_context_name_type iter_hyp pfctxt +(* FIXME: this is a Libobject hack that should be replaced with a proper + registration mechanism. *) +module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> unit end) + +let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with +| f -> f o +| exception Not_found -> () + (* General search over declarations *) let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) = let env = Global.env () in @@ -78,13 +86,14 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) = (Environ.named_context env); let iter_obj (sp, kn) lobj = match lobj with | AtomicObject o -> - begin match object_tag o with - | "CONSTANT" -> + let handler = + DynHandle.add Declare.Internal.objConstant begin fun _ -> let cst = Global.constant_of_delta_kn kn in let gr = GlobRef.ConstRef cst in let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in fn gr env typ - | "INDUCTIVE" -> + end @@ + DynHandle.add DeclareInd.Internal.objInductive begin fun _ -> let mind = Global.mind_of_delta_kn kn in let mib = Global.lookup_mind mind in let iter_packet i mip = @@ -97,8 +106,10 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) = iter_constructors ind u fn env len in Array.iteri iter_packet mib.mind_packets - | _ -> () - end + end @@ + DynHandle.empty + in + handle handler o | _ -> () in try Declaremods.iter_all_segments iter_obj diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 45f40b1258..de02f7ecfb 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -359,7 +359,7 @@ let in_phase ~phase f x = default_phase := op; res with exn -> - let iexn = Backtrace.add_backtrace exn in + let iexn = Exninfo.capture exn in default_phase := op; Util.iraise iexn @@ -415,7 +415,7 @@ let with_output_to_file fname func input = close_out channel; output with reraise -> - let reraise = Backtrace.add_backtrace reraise in + let reraise = Exninfo.capture reraise in std_ft := Util.pi1 old_fmt; err_ft := Util.pi2 old_fmt; deep_ft := Util.pi3 old_fmt; diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 7b4924eaed..6e398d87ca 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -19,11 +19,9 @@ DeclareObl Canonical RecLemmas Library -Prettyp Lemmas ComCoercion Auto_ind_decl -Search Indschemes Obligations ComDefinition @@ -31,6 +29,8 @@ Classes ComPrimitive ComAssumption DeclareInd +Search +Prettyp ComInductive ComFixpoint ComProgramFixpoint diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e98820bc98..f8eef68997 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -609,27 +609,8 @@ let vernac_assumption ~atts discharge kind l nl = | DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l; ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l -let set_template_check b = - let typing_flags = Environ.typing_flags (Global.env ()) in - Global.set_typing_flags { typing_flags with Declarations.check_template = b } - -let is_template_check () = - let typing_flags = Environ.typing_flags (Global.env ()) in - typing_flags.Declarations.check_template - -let () = - let tccheck = - { optdepr = true; - optname = "Template universe check"; - optkey = ["Template"; "Check"]; - optread = (fun () -> is_template_check ()); - optwrite = (fun b -> set_template_check b)} - in - declare_bool_option tccheck - let is_polymorphic_inductive_cumulativity = declare_bool_option_and_ref ~depr:false ~value:false - ~name:"Polymorphic inductive cumulativity" ~key:["Polymorphic"; "Inductive"; "Cumulativity"] let should_treat_as_cumulative cum poly = @@ -645,7 +626,6 @@ let should_treat_as_cumulative cum poly = let get_uniform_inductive_parameters = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"Uniform inductive parameters" ~key:["Uniform"; "Inductive"; "Parameters"] ~value:false @@ -1238,7 +1218,6 @@ let vernac_generalizable ~local = let () = declare_bool_option { optdepr = false; - optname = "allow sprop"; optkey = ["Allow";"StrictProp"]; optread = (fun () -> Global.sprop_allowed()); optwrite = Global.set_allow_sprop } @@ -1246,7 +1225,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "silent"; optkey = ["Silent"]; optread = (fun () -> !Flags.quiet); optwrite = ((:=) Flags.quiet) } @@ -1254,7 +1232,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "implicit arguments"; optkey = ["Implicit";"Arguments"]; optread = Impargs.is_implicit_args; optwrite = Impargs.make_implicit_args } @@ -1262,7 +1239,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "strict implicit arguments"; optkey = ["Strict";"Implicit"]; optread = Impargs.is_strict_implicit_args; optwrite = Impargs.make_strict_implicit_args } @@ -1270,7 +1246,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "strong strict implicit arguments"; optkey = ["Strongly";"Strict";"Implicit"]; optread = Impargs.is_strongly_strict_implicit_args; optwrite = Impargs.make_strongly_strict_implicit_args } @@ -1278,7 +1253,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "contextual implicit arguments"; optkey = ["Contextual";"Implicit"]; optread = Impargs.is_contextual_implicit_args; optwrite = Impargs.make_contextual_implicit_args } @@ -1286,7 +1260,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "implicit status of reversible patterns"; optkey = ["Reversible";"Pattern";"Implicit"]; optread = Impargs.is_reversible_pattern_implicit_args; optwrite = Impargs.make_reversible_pattern_implicit_args } @@ -1294,7 +1267,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "maximal insertion of implicit"; optkey = ["Maximal";"Implicit";"Insertion"]; optread = Impargs.is_maximal_implicit_args; optwrite = Impargs.make_maximal_implicit_args } @@ -1302,7 +1274,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "coercion printing"; optkey = ["Printing";"Coercions"]; optread = (fun () -> !Constrextern.print_coercions); optwrite = (fun b -> Constrextern.print_coercions := b) } @@ -1310,7 +1281,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "printing of existential variable instances"; optkey = ["Printing";"Existential";"Instances"]; optread = (fun () -> !Detyping.print_evar_arguments); optwrite = (:=) Detyping.print_evar_arguments } @@ -1318,7 +1288,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "implicit arguments printing"; optkey = ["Printing";"Implicit"]; optread = (fun () -> !Constrextern.print_implicits); optwrite = (fun b -> Constrextern.print_implicits := b) } @@ -1326,7 +1295,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "implicit arguments defensive printing"; optkey = ["Printing";"Implicit";"Defensive"]; optread = (fun () -> !Constrextern.print_implicits_defensive); optwrite = (fun b -> Constrextern.print_implicits_defensive := b) } @@ -1334,7 +1302,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "projection printing using dot notation"; optkey = ["Printing";"Projections"]; optread = (fun () -> !Constrextern.print_projections); optwrite = (fun b -> Constrextern.print_projections := b) } @@ -1342,7 +1309,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "notations printing"; optkey = ["Printing";"Notations"]; optread = (fun () -> not !Constrextern.print_no_symbol); optwrite = (fun b -> Constrextern.print_no_symbol := not b) } @@ -1350,7 +1316,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "raw printing"; optkey = ["Printing";"All"]; optread = (fun () -> !Flags.raw_print); optwrite = (fun b -> Flags.raw_print := b) } @@ -1358,7 +1323,6 @@ let () = let () = declare_int_option { optdepr = false; - optname = "the level of inlining during functor application"; optkey = ["Inline";"Level"]; optread = (fun () -> Some (Flags.get_inline_level ())); optwrite = (fun o -> @@ -1368,7 +1332,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "kernel term sharing"; optkey = ["Kernel"; "Term"; "Sharing"]; optread = (fun () -> (Global.typing_flags ()).Declarations.share_reduction); optwrite = Global.set_share_reduction } @@ -1376,7 +1339,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "display compact goal contexts"; optkey = ["Printing";"Compact";"Contexts"]; optread = (fun () -> Printer.get_compact_context()); optwrite = (fun b -> Printer.set_compact_context b) } @@ -1384,7 +1346,6 @@ let () = let () = declare_int_option { optdepr = false; - optname = "the printing depth"; optkey = ["Printing";"Depth"]; optread = Topfmt.get_depth_boxes; optwrite = Topfmt.set_depth_boxes } @@ -1392,7 +1353,6 @@ let () = let () = declare_int_option { optdepr = false; - optname = "the printing width"; optkey = ["Printing";"Width"]; optread = Topfmt.get_margin; optwrite = Topfmt.set_margin } @@ -1400,7 +1360,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "printing of universes"; optkey = ["Printing";"Universes"]; optread = (fun () -> !Constrextern.print_universes); optwrite = (fun b -> Constrextern.print_universes:=b) } @@ -1408,7 +1367,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "dumping bytecode after compilation"; optkey = ["Dump";"Bytecode"]; optread = (fun () -> !Cbytegen.dump_bytecode); optwrite = (:=) Cbytegen.dump_bytecode } @@ -1416,7 +1374,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "dumping VM lambda code after compilation"; optkey = ["Dump";"Lambda"]; optread = (fun () -> !Clambda.dump_lambda); optwrite = (:=) Clambda.dump_lambda } @@ -1424,7 +1381,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "explicitly parsing implicit arguments"; optkey = ["Parsing";"Explicit"]; optread = (fun () -> !Constrintern.parsing_explicit); optwrite = (fun b -> Constrintern.parsing_explicit := b) } @@ -1432,7 +1388,6 @@ let () = let () = declare_string_option ~preprocess:CWarnings.normalize_flags_string { optdepr = false; - optname = "warnings display"; optkey = ["Warnings"]; optread = CWarnings.get_flags; optwrite = CWarnings.set_flags } @@ -1440,7 +1395,6 @@ let () = let () = declare_string_option { optdepr = false; - optname = "native_compute profiler output"; optkey = ["NativeCompute"; "Profile"; "Filename"]; optread = Nativenorm.get_profile_filename; optwrite = Nativenorm.set_profile_filename } @@ -1448,15 +1402,20 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "enable native compute profiling"; optkey = ["NativeCompute"; "Profiling"]; optread = Nativenorm.get_profiling_enabled; optwrite = Nativenorm.set_profiling_enabled } +let () = + declare_bool_option + { optdepr = false; + optkey = ["NativeCompute"; "Timing"]; + optread = Nativenorm.get_timing_enabled; + optwrite = Nativenorm.set_timing_enabled } + let _ = declare_bool_option { optdepr = false; - optname = "guard checking"; optkey = ["Guard"; "Checking"]; optread = (fun () -> (Global.typing_flags ()).Declarations.check_guarded); optwrite = (fun b -> Global.set_check_guarded b) } @@ -1464,7 +1423,6 @@ let _ = let _ = declare_bool_option { optdepr = false; - optname = "positivity/productivity checking"; optkey = ["Positivity"; "Checking"]; optread = (fun () -> (Global.typing_flags ()).Declarations.check_positive); optwrite = (fun b -> Global.set_check_positive b) } @@ -1472,7 +1430,6 @@ let _ = let _ = declare_bool_option { optdepr = false; - optname = "universes checking"; optkey = ["Universe"; "Checking"]; optread = (fun () -> (Global.typing_flags ()).Declarations.check_universes); optwrite = (fun b -> Global.set_check_universes b) } @@ -1581,7 +1538,7 @@ let query_command_selector ?loc = function let vernac_check_may_eval ~pstate ~atts redexp glopt rc = let glopt = query_command_selector glopt in let sigma, env = get_current_context_of_args ~pstate glopt in - let sigma, c = interp_open_constr env sigma rc in + let sigma, c = interp_open_constr ~expected_type:Pretyping.UnknownIfTermOrType env sigma rc in let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in Evarconv.check_problems_are_solved env sigma; let sigma = Evd.minimize_universes sigma in @@ -1787,7 +1744,6 @@ let search_output_name_only = ref false let () = declare_bool_option { optdepr = false; - optname = "output-name-only search"; optkey = ["Search";"Output";"Name";"Only"]; optread = (fun () -> !search_output_name_only); optwrite = (:=) search_output_name_only } diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 1daa244986..22a8de7f99 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -254,7 +254,7 @@ type vernac_one_argument_status = { name : Name.t; recarg_like : bool; notation_scope : string CAst.t option; - implicit_status : Impargs.implicit_kind; + implicit_status : Glob_term.binding_kind; } type vernac_argument_status = @@ -386,7 +386,7 @@ type nonrec vernac_expr = | VernacArguments of qualid or_by_notation * vernac_argument_status list (* Main arguments status list *) * - (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) * + (Name.t * Glob_term.binding_kind) list list (* Extra implicit status lists *) * arguments_modifier list | VernacReserve of simple_binder list | VernacGeneralizable of (lident list) option diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index c14fc78462..1ec09b6beb 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -65,7 +65,6 @@ let proof_mode_opt_name = ["Default";"Proof";"Mode"] let () = Goptions.declare_string_option Goptions.{ optdepr = false; - optname = "default proof mode" ; optkey = proof_mode_opt_name; optread = get_default_proof_mode_opt; optwrite = set_default_proof_mode_opt; @@ -249,7 +248,6 @@ let interp_qed_delayed_control ~proof ~info ~st ~control { CAst.loc; v=pe } = let () = let open Goptions in declare_int_option { optdepr = false; - optname = "the default timeout"; optkey = ["Default";"Timeout"]; optread = (fun () -> !default_timeout); optwrite = ((:=) default_timeout) } diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index c81a4abc1b..80b72225f0 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -124,7 +124,7 @@ module Proof_global = struct let () = CErrors.register_handler begin function | NoCurrentProof -> - CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).") + Pp.(str "No focused proof (No proof-editing in progress).") | _ -> raise CErrors.Unhandled end |