diff options
Diffstat (limited to 'plugins')
50 files changed, 166 insertions, 183 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index a6f432b5bd..575d964158 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -33,7 +33,7 @@ let print_constr t = let debug x = if !cc_verbose then Feedback.msg_debug (x ()) -let _= +let () = let gdopt= { optdepr=false; optname="Congruence Verbose"; @@ -61,7 +61,7 @@ module ST=struct type t = {toterm: int IntPairTable.t; tosign: (int * int) IntTable.t} - let empty ()= + let empty () = {toterm=IntPairTable.create init_size; tosign=IntTable.create init_size} @@ -321,7 +321,7 @@ let compress_path uf i j = uf.map.(j).cpath<-i let rec find_aux uf visited i= let j = uf.map.(i).cpath in - if j<0 then let _ = List.iter (compress_path uf i) visited in i else + if j<0 then let () = List.iter (compress_path uf i) visited in i else find_aux uf (i::visited) j let find uf i= find_aux uf [] i diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index f6eea3c5c4..16890ea260 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -500,7 +500,7 @@ let info_file f = let my_bool_option name initval = let flag = ref initval in let access = fun () -> !flag in - let _ = declare_bool_option + let () = declare_bool_option {optdepr = false; optname = "Extraction "^name; optkey = ["Extraction"; name]; @@ -572,14 +572,14 @@ let chg_flag n = int_flag_ref := n; opt_flag_ref := flag_of_int n let optims () = !opt_flag_ref -let _ = declare_bool_option +let () = declare_bool_option {optdepr = false; optname = "Extraction Optimize"; optkey = ["Extraction"; "Optimize"]; optread = (fun () -> not (Int.equal !int_flag_ref 0)); optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))} -let _ = declare_int_option +let () = declare_int_option { optdepr = false; optname = "Extraction Flag"; optkey = ["Extraction";"Flag"]; @@ -593,7 +593,7 @@ let _ = declare_int_option let conservative_types_ref = ref false let conservative_types () = !conservative_types_ref -let _ = declare_bool_option +let () = declare_bool_option {optdepr = false; optname = "Extraction Conservative Types"; optkey = ["Extraction"; "Conservative"; "Types"]; @@ -605,7 +605,7 @@ let _ = declare_bool_option let file_comment_ref = ref "" let file_comment () = !file_comment_ref -let _ = declare_string_option +let () = declare_string_option {optdepr = false; optname = "Extraction File Comment"; optkey = ["Extraction"; "File"; "Comment"]; diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index a212d13453..37fc81ee38 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -33,7 +33,7 @@ DECLARE PLUGIN "ground_plugin" let ground_depth=ref 3 -let _= +let ()= let gdopt= { optdepr=false; optname="Firstorder Depth"; @@ -47,7 +47,7 @@ let _= declare_int_option gdopt -let _= +let ()= let congruence_depth=ref 100 in let gdopt= { optdepr=true; (* noop *) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ef1d1af199..3b95423067 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1005,8 +1005,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (mk_equation_id f_id) (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem)) evd - lemma_type - (Lemmas.mk_hook (fun _ _ -> ())); + lemma_type; ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))); evd diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 1cf952576d..4cdfc6fac5 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -310,7 +310,6 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) !evd (EConstr.of_constr new_principle_type) - hook ; (* let _tim1 = System.get_time () in *) let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in @@ -322,11 +321,11 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* end; *) let open Proof_global in - let { id; entries; persistence } = fst @@ close_proof ~keep_body_ucst_separate:false (fun x -> x) in + let { id; entries; persistence } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) in match entries with | [entry] -> discard_current (); - (id,(entry,persistence)), CEphemeron.create hook + (id,(entry,persistence)), hook | _ -> CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term") end @@ -386,7 +385,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) (* Pr 1278 : Don't forget to close the goal if an error is raised !!!! *) - save false new_princ_name entry g_kind hook + save false new_princ_name entry g_kind ~hook with e when CErrors.noncritical e -> begin begin diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 7e707b423a..8f0440a2a4 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -145,7 +145,6 @@ END { -module Gram = Pcoq.Gram module Vernac = Pvernac.Vernac_ module Tactic = Pltac diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 35acbea488..3a04c753ea 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -415,7 +415,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp ~program_mode:false fname (Decl_kinds.Global,false,Decl_kinds.Definition) pl - bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); + bl None body (Some ret_type); let evd,rev_pconstants = List.fold_left (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index b68b34ca35..19f954c10d 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -129,7 +129,7 @@ let get_locality = function | Local -> true | Global -> false -let save with_clean id const (locality,_,kind) hook = +let save with_clean id const ?hook (locality,_,kind) = let fix_exn = Future.fix_exn_of const.const_entry_body in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> @@ -144,7 +144,7 @@ let save with_clean id const (locality,_,kind) hook = (locality, ConstRef kn) in if with_clean then Proof_global.discard_current (); - CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); + Lemmas.call_hook ?hook ~fix_exn l r; definition_message id let with_full_print f a = @@ -375,7 +375,7 @@ let functional_induction_rewrite_dependent_proofs_sig = optread = (fun () -> !functional_induction_rewrite_dependent_proofs); optwrite = (fun b -> functional_induction_rewrite_dependent_proofs := b) } -let _ = declare_bool_option functional_induction_rewrite_dependent_proofs_sig +let () = declare_bool_option functional_induction_rewrite_dependent_proofs_sig let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = true @@ -388,7 +388,7 @@ let function_debug_sig = optwrite = (fun b -> function_debug := b) } -let _ = declare_bool_option function_debug_sig +let () = declare_bool_option function_debug_sig let do_observe () = !function_debug @@ -406,7 +406,7 @@ let strict_tcc_sig = optwrite = (fun b -> strict_tcc := b) } -let _ = declare_bool_option strict_tcc_sig +let () = declare_bool_option strict_tcc_sig exception Building_graph of exn diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index c9d153d89f..9584649cff 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -42,8 +42,7 @@ val const_of_id: Id.t -> GlobRef.t(* constantyes *) val jmeq : unit -> EConstr.constr val jmeq_refl : unit -> EConstr.constr -val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind -> - Lemmas.declaration_hook CEphemeron.key -> unit +val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> ?hook:Lemmas.declaration_hook -> Decl_kinds.goal_kind -> unit (* [with_full_print f a] applies [f] to [a] in full printing environment. diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d1a227d517..95e2e9f6e5 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -806,8 +806,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list lem_id (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem))) !evd - typ - (Lemmas.mk_hook (fun _ _ -> ())); + typ; ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") (proving_tac i)))); @@ -867,8 +866,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let lem_id = mk_complete_id f_id in Lemmas.start_proof lem_id (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma - (fst lemmas_types_infos.(i)) - (Lemmas.mk_hook (fun _ _ -> ())); + (fst lemmas_types_infos.(i)); ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i)))) ; diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 6e5e3f9353..38f27f760b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1372,7 +1372,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp na (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma) sigma gls_type - (Lemmas.mk_hook hook); + ~hook:(Lemmas.mk_hook hook); if Indfun_common.is_strict_tcc () then ignore (by (Proofview.V82.tactic (tclIDTAC))) @@ -1418,7 +1418,7 @@ let com_terminate let evd, env = Pfedit.get_current_context () in Lemmas.start_proof thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) - ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook; + ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook; ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start))); ignore (by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref @@ -1474,8 +1474,7 @@ let (com_eqn : int -> Id.t -> (Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign:(Environ.named_context_val env) evd - (EConstr.of_constr equation_lemma_type) - (Lemmas.mk_hook (fun _ _ -> ())); + (EConstr.of_constr equation_lemma_type); ignore (by (Proofview.V82.tactic (start_equation f_ref terminate_ref (fun x -> diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index c4c4e51ecc..156ee94a66 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -332,7 +332,7 @@ END let local_test_lpar_id_colon = let err () = raise Stream.Failure in - Pcoq.Gram.Entry.of_parser "lpar_id_colon" + Pcoq.Entry.of_parser "lpar_id_colon" (fun strm -> match Util.stream_nth 0 strm with | Tok.KEYWORD "(" -> diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index fa70235975..0509d6ae71 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Genintern open Tacexpr open Names open Constrexpr @@ -28,22 +29,22 @@ val wit_natural : int Genarg.uniform_genarg_type val wit_glob : (constr_expr, - Tacexpr.glob_constr_and_expr, + glob_constr_and_expr, Tacinterp.interp_sign * glob_constr) Genarg.genarg_type val wit_lglob : (constr_expr, - Tacexpr.glob_constr_and_expr, + glob_constr_and_expr, Tacinterp.interp_sign * glob_constr) Genarg.genarg_type val wit_lconstr : (constr_expr, - Tacexpr.glob_constr_and_expr, + glob_constr_and_expr, EConstr.t) Genarg.genarg_type val wit_casted_constr : (constr_expr, - Tacexpr.glob_constr_and_expr, + glob_constr_and_expr, EConstr.t) Genarg.genarg_type val glob : constr_expr Pcoq.Entry.t diff --git a/plugins/ltac/extratactics.mli b/plugins/ltac/extratactics.mli index 7fb9a19a0c..4576562634 100644 --- a/plugins/ltac/extratactics.mli +++ b/plugins/ltac/extratactics.mli @@ -14,4 +14,4 @@ val injHyp : Names.Id.t -> unit Proofview.tactic (* val refine_tac : Evd.open_constr -> unit Proofview.tactic *) -val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Tacexpr.delayed_open option -> unit Proofview.tactic +val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Tactypes.delayed_open option -> unit Proofview.tactic diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index bd8a097154..d9b19c1ae6 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -70,7 +70,7 @@ let _ = (* Hack to parse "[ id" without dropping [ *) let test_bracket_ident = - Gram.Entry.of_parser "test_bracket_ident" + Pcoq.Entry.of_parser "test_bracket_ident" (fun strm -> match stream_nth 0 strm with | KEYWORD "[" -> @@ -373,7 +373,7 @@ open Libnames let print_info_trace = ref None -let _ = declare_int_option { +let () = declare_int_option { optdepr = false; optname = "print info trace"; optkey = ["Info" ; "Level"]; diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index e29f78af5b..ef18dd6cdc 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -45,7 +45,6 @@ let with_tac f tac = * Subtac. These entries are named Subtac.<foo> *) -module Gram = Pcoq.Gram module Tactic = Pltac open Pcoq diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 2596bc22f2..31fb1c9abf 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -16,6 +16,7 @@ open Names open Locus open Constrexpr open Glob_term +open Genintern open Geninterp open Extraargs open Tacmach @@ -37,8 +38,8 @@ DECLARE PLUGIN "ltac_plugin" { type constr_expr_with_bindings = constr_expr with_bindings -type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings -type glob_constr_with_bindings_sign = interp_sign * Tacexpr.glob_constr_and_expr with_bindings +type glob_constr_with_bindings = glob_constr_and_expr with_bindings +type glob_constr_with_bindings_sign = interp_sign * glob_constr_and_expr with_bindings let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = let _, env = Pfedit.get_current_context () in @@ -70,7 +71,7 @@ END { type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast -type glob_strategy = (Tacexpr.glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast +type glob_strategy = (glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast let interp_strategy ist gl s = let sigma = project gl in @@ -226,8 +227,6 @@ let () = let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer -open Pcoq - } GRAMMAR EXTEND Gram diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 0ce0fbd0cd..46ea3819ac 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -39,7 +39,7 @@ let err () = raise Stream.Failure (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) (* admissible notation "(x t)" *) let test_lpar_id_coloneq = - Gram.Entry.of_parser "lpar_id_coloneq" + Pcoq.Entry.of_parser "lpar_id_coloneq" (fun strm -> match stream_nth 0 strm with | KEYWORD "(" -> @@ -53,7 +53,7 @@ let test_lpar_id_coloneq = (* Hack to recognize "(x)" *) let test_lpar_id_rpar = - Gram.Entry.of_parser "lpar_id_coloneq" + Pcoq.Entry.of_parser "lpar_id_coloneq" (fun strm -> match stream_nth 0 strm with | KEYWORD "(" -> @@ -67,7 +67,7 @@ let test_lpar_id_rpar = (* idem for (x:=t) and (1:=t) *) let test_lpar_idnum_coloneq = - Gram.Entry.of_parser "test_lpar_idnum_coloneq" + Pcoq.Entry.of_parser "test_lpar_idnum_coloneq" (fun strm -> match stream_nth 0 strm with | KEYWORD "(" -> @@ -84,7 +84,7 @@ open Extraargs (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *) let check_for_coloneq = - Gram.Entry.of_parser "lpar_id_colon" + Pcoq.Entry.of_parser "lpar_id_colon" (fun strm -> let rec skip_to_rpar p n = match List.last (Stream.npeek n strm) with @@ -108,7 +108,7 @@ let check_for_coloneq = | _ -> err ()) let lookup_at_as_comma = - Gram.Entry.of_parser "lookup_at_as_comma" + Pcoq.Entry.of_parser "lookup_at_as_comma" (fun strm -> match stream_nth 0 strm with | KEYWORD (","|"at"|"as") -> () diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 50cfb6d004..55e58187b0 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -26,6 +26,7 @@ open Pputils open Ppconstr open Printer +open Genintern open Tacexpr open Tacarg open Tactics diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 6c09e447a5..0ab9e501bc 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -17,6 +17,7 @@ open Names open Environ open Constrexpr open Notation_gram +open Genintern open Tacexpr open Tactypes diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 3eb049dbab..ae4b53325f 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -446,7 +446,7 @@ let do_print_results_at_close () = let _ = Declaremods.append_end_library_hook do_print_results_at_close -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index fee469032c..06783de614 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1998,7 +1998,7 @@ let add_morphism_infer atts m n = let hook = Lemmas.mk_hook hook in Flags.silently (fun () -> - Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) hook; + Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance); ignore (Pfedit.by (Tacinterp.interp tac))) () let add_morphism atts binders m s n = diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 4f46e78c71..2457b265f0 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -13,6 +13,7 @@ open Environ open EConstr open Constrexpr open Evd +open Genintern open Tactypes open Tacexpr open Tacinterp diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index bdb0be03cf..0c7096a4de 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -11,6 +11,7 @@ open Genarg open EConstr open Constrexpr +open Genintern open Tactypes open Tacexpr diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index d2ae92f6ce..b04c3b9f4e 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -53,7 +53,7 @@ val coerce_var_to_ident : bool -> Environ.env -> Evd.evar_map -> Value.t -> Id.t val coerce_to_ident_not_fresh : Evd.evar_map -> Value.t -> Id.t -val coerce_to_intro_pattern : Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr +val coerce_to_intro_pattern : Evd.evar_map -> Value.t -> delayed_open_constr intro_pattern_expr val coerce_to_intro_pattern_naming : Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index ac2d88dec2..2aee809eb6 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -119,7 +119,7 @@ let get_tactic_entry n = else if Int.equal n 5 then Pltac.binder_tactic, None else if 1<=n && n<5 then - Pltac.tactic_expr, Some (Extend.Level (string_of_int n)) + Pltac.tactic_expr, Some (Gramlib.Gramext.Level (string_of_int n)) else user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^".")) diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 9435d0b911..2bd21f9d7a 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -93,19 +93,8 @@ type ml_tactic_entry = { (** Composite types *) -type glob_constr_and_expr = Genintern.glob_constr_and_expr - type open_constr_expr = unit * constr_expr -type open_glob_constr = unit * glob_constr_and_expr - -type binding_bound_vars = Constr_matching.binding_bound_vars -type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern - -type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a - -type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open - -type delayed_open_constr = EConstr.constr delayed_open +type open_glob_constr = unit * Genintern.glob_constr_and_expr type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list @@ -279,8 +268,8 @@ constraint 'a = < (** Globalized tactics *) -type g_trm = glob_constr_and_expr -type g_pat = glob_constr_pattern_and_expr +type g_trm = Genintern.glob_constr_and_expr +type g_pat = Genintern.glob_constr_pattern_and_expr type g_cst = evaluable_global_reference Stdarg.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 1527724420..0c27f3bfe2 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -92,20 +92,8 @@ type ml_tactic_entry = { } (** Composite types *) - -type glob_constr_and_expr = Genintern.glob_constr_and_expr - type open_constr_expr = unit * constr_expr -type open_glob_constr = unit * glob_constr_and_expr - -type binding_bound_vars = Constr_matching.binding_bound_vars -type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern - -type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a - -type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open - -type delayed_open_constr = EConstr.constr delayed_open +type open_glob_constr = unit * Genintern.glob_constr_and_expr type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list @@ -279,8 +267,8 @@ constraint 'a = < (** Globalized tactics *) -type g_trm = glob_constr_and_expr -type g_pat = glob_constr_pattern_and_expr +type g_trm = Genintern.glob_constr_and_expr +type g_pat = Genintern.glob_constr_pattern_and_expr type g_cst = evaluable_global_reference Stdarg.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index 178f6af71d..978ad4dd24 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -12,6 +12,7 @@ open Names open Tacexpr open Genarg open Constrexpr +open Genintern open Tactypes (** Globalization of tactic expressions : diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index cb3a0aaed9..cf5eb442be 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2039,7 +2039,7 @@ let _ = let vernac_debug b = set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; @@ -2048,13 +2048,4 @@ let _ = optread = (fun () -> get_debug () != Tactic_debug.DebugOff); optwrite = vernac_debug } -let _ = - let open Goptions in - declare_bool_option - { optdepr = false; - optname = "Ltac debug"; - optkey = ["Debug";"Ltac"]; - optread = (fun () -> get_debug () != Tactic_debug.DebugOff); - optwrite = vernac_debug } - let () = Hook.set Vernacentries.interp_redexp_hook interp_redexp diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index f9883e4441..d9c80bb835 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -43,6 +43,8 @@ type interp_sign = Geninterp.interp_sign = { lfun : value Id.Map.t; extra : TacStore.t } +open Genintern + val f_avoid_ids : Id.Set.t TacStore.field val f_debug : debug_info TacStore.field diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli index d406686c56..4487604dca 100644 --- a/plugins/ltac/tacsubst.mli +++ b/plugins/ltac/tacsubst.mli @@ -11,6 +11,7 @@ open Tacexpr open Mod_subst open Genarg +open Genintern open Tactypes (** Substitution of tactics at module closing time *) diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 877d4ee758..99b9e881f6 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -89,7 +89,7 @@ let batch = ref false open Goptions -let _ = +let () = declare_bool_option { optdepr = false; optname = "Ltac batch debug"; diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 175341df09..91e8510b92 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -40,7 +40,7 @@ val db_constr : debug_info -> env -> evar_map -> constr -> unit Proofview.NonLog (** Prints the pattern rule *) val db_pattern_rule : - debug_info -> int -> (Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t + debug_info -> int -> (Genintern.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t (** Prints a matched hypothesis *) val db_matched_hyp : diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli index 0722c68783..457c4e0b9a 100644 --- a/plugins/ltac/tactic_matching.mli +++ b/plugins/ltac/tactic_matching.mli @@ -35,7 +35,7 @@ val match_term : Environ.env -> Evd.evar_map -> EConstr.constr -> - (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> + (Constr_matching.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> Tacexpr.glob_tactic_expr t Proofview.tactic (** [match_goal env sigma hyps concl rules] matches the goal @@ -48,5 +48,5 @@ val match_goal: Evd.evar_map -> EConstr.named_context -> EConstr.constr -> - (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> + (Constr_matching.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> Tacexpr.glob_tactic_expr t Proofview.tactic diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 561bfc5d7c..19256e054d 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -65,7 +65,7 @@ let assoc_flags ist : tauto_flags = let negation_unfolding = ref true open Goptions -let _ = +let () = declare_bool_option { optdepr = false; optname = "unfolding of not in intuition"; diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 402e8b91e6..d4bafe773f 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -51,7 +51,7 @@ let get_lra_option () = -let _ = +let () = let int_opt l vref = { @@ -89,11 +89,11 @@ let _ = optwrite = (fun x -> Certificate.dump_file := x) } in - let _ = declare_bool_option solver_opt in - let _ = declare_stringopt_option dump_file_opt in - let _ = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in - let _ = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in - let _ = declare_bool_option lia_enum_opt in + let () = declare_bool_option solver_opt in + let () = declare_stringopt_option dump_file_opt in + let () = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in + let () = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in + let () = declare_bool_option lia_enum_opt in () diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index d8adb17710..dff25b3a42 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -64,7 +64,7 @@ let write f x = f:=x open Goptions -let _ = +let () = declare_bool_option { optdepr = false; optname = "Omega system time displaying flag"; @@ -72,7 +72,7 @@ let _ = optread = read display_system_flag; optwrite = write display_system_flag } -let _ = +let () = declare_bool_option { optdepr = false; optname = "Omega action display flag"; @@ -80,7 +80,7 @@ let _ = optread = read display_action_flag; optwrite = write display_action_flag } -let _ = +let () = declare_bool_option { optdepr = false; optname = "Omega old style flag"; @@ -88,7 +88,7 @@ let _ = optread = read old_style_flag; optwrite = write old_style_flag } -let _ = +let () = declare_bool_option { optdepr = true; optname = "Omega automatic reset of generated names"; @@ -96,7 +96,7 @@ let _ = optread = read reset_flag; optwrite = write reset_flag } -let _ = +let () = declare_bool_option { optdepr = false; optname = "Omega takes advantage of context variables with body"; diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 3de5923968..aab1e47555 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -54,7 +54,7 @@ let opt_pruning= optread=(fun () -> !pruning); optwrite=(fun b -> pruning:=b)} -let _ = declare_bool_option opt_pruning +let () = declare_bool_option opt_pruning type form= Atom of int diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 840a05e02b..e66fa10d5b 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -236,7 +236,7 @@ let opt_verbose= optread=(fun () -> !verbose); optwrite=(fun b -> verbose:=b)} -let _ = declare_bool_option opt_verbose +let () = declare_bool_option opt_verbose let check = ref false @@ -247,7 +247,7 @@ let opt_check= optread=(fun () -> !check); optwrite=(fun b -> check:=b)} -let _ = declare_bool_option opt_check +let () = declare_bool_option opt_check open Pp @@ -255,7 +255,7 @@ let rtauto_tac gls= Coqlib.check_required_library ["Coq";"rtauto";"Rtauto"]; let gamma={next=1;env=[]} in let gl=pf_concl gls in - let _= + let () = if Retyping.get_sort_family_of (pf_env gls) (Tacmach.project gls) gl != InProp then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in @@ -267,7 +267,7 @@ let rtauto_tac gls= | Tactic_debug.DebugOn 0 -> Search.debug_depth_first | _ -> Search.depth_first in - let _ = + let () = begin reset_info (); if !verbose then @@ -279,7 +279,7 @@ let rtauto_tac gls= with Not_found -> user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in let search_end_time = System.get_time () in - let _ = if !verbose then + let () = if !verbose then begin Feedback.msg_info (str "Proof tree found in " ++ System.fmt_time_difference search_start_time search_end_time); @@ -287,7 +287,7 @@ let rtauto_tac gls= Feedback.msg_info (str "Building proof term ... ") end in let build_start_time=System.get_time () in - let _ = step_count := 0; node_count := 0 in + let () = step_count := 0; node_count := 0 in let main = mkApp (force node_count l_Reflect, [|build_env gamma; build_form formula; @@ -295,7 +295,7 @@ let rtauto_tac gls= let term= applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in let build_end_time=System.get_time () in - let _ = if !verbose then + let () = if !verbose then begin Feedback.msg_info (str "Proof term built in " ++ System.fmt_time_difference build_start_time build_end_time ++ @@ -314,7 +314,7 @@ let rtauto_tac gls= else Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in let tac_end_time = System.get_time () in - let _ = + let () = if !check then Feedback.msg_info (str "Proof term type-checking is on"); if !verbose then Feedback.msg_info (str "Internal tactic executed in " ++ diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index a786b9953d..bb8a0faf2e 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -47,7 +47,7 @@ type ssrdocc = ssrclear option * ssrocc (* OLD ssr terms *) type ssrtermkind = char (* FIXME, make algebraic *) -type ssrterm = ssrtermkind * Tacexpr.glob_constr_and_expr +type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr (* NEW ssr term *) diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index e25c93bf0a..824827e90c 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -146,7 +146,7 @@ val interp_refine : val interp_open_constr : Tacinterp.interp_sign -> Goal.goal Evd.sigma -> - Tacexpr.glob_constr_and_expr -> evar_map * (evar_map * EConstr.t) + Genintern.glob_constr_and_expr -> evar_map * (evar_map * EConstr.t) val pf_e_type_of : Goal.goal Evd.sigma -> diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 22475fef34..490e8fbdbc 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -32,13 +32,13 @@ open Tacticals open Tacmach let ssroldreworder = Summary.ref ~name:"SSR:oldreworder" false -let _ = - Goptions.declare_bool_option - { Goptions.optname = "ssreflect 1.3 compatibility flag"; - Goptions.optkey = ["SsrOldRewriteGoalsOrder"]; - Goptions.optread = (fun _ -> !ssroldreworder); - Goptions.optdepr = false; - Goptions.optwrite = (fun b -> ssroldreworder := b) } +let () = + Goptions.(declare_bool_option + { optname = "ssreflect 1.3 compatibility flag"; + optkey = ["SsrOldRewriteGoalsOrder"]; + optread = (fun _ -> !ssroldreworder); + optdepr = false; + optwrite = (fun b -> ssroldreworder := b) }) (** The "simpl" tactic *) diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index f67cf20e49..8cebe62e16 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -66,14 +66,14 @@ open Ssripats let ssrhaveNOtcresolution = Summary.ref ~name:"SSR:havenotcresolution" false -let _ = - Goptions.declare_bool_option - { Goptions.optname = "have type classes"; - Goptions.optkey = ["SsrHave";"NoTCResolution"]; - Goptions.optread = (fun _ -> !ssrhaveNOtcresolution); - Goptions.optdepr = false; - Goptions.optwrite = (fun b -> ssrhaveNOtcresolution := b); - } +let () = + Goptions.(declare_bool_option + { optname = "have type classes"; + optkey = ["SsrHave";"NoTCResolution"]; + optread = (fun _ -> !ssrhaveNOtcresolution); + optdepr = false; + optwrite = (fun b -> ssrhaveNOtcresolution := b); + }) open Constrexpr diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 7c91860228..c9221ef758 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -268,16 +268,16 @@ let negate_parser f x = | Some _ -> raise Stream.Failure let test_not_ssrslashnum = - Pcoq.Gram.Entry.of_parser + Pcoq.Entry.of_parser "test_not_ssrslashnum" (negate_parser test_ssrslashnum10) let test_ssrslashnum00 = - Pcoq.Gram.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00 + Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00 let test_ssrslashnum10 = - Pcoq.Gram.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10 + Pcoq.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10 let test_ssrslashnum11 = - Pcoq.Gram.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11 + Pcoq.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11 let test_ssrslashnum01 = - Pcoq.Gram.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01 + Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01 } @@ -470,7 +470,7 @@ let input_ssrtermkind strm = match Util.stream_nth 0 strm with | Tok.KEYWORD "@" -> xWithAt | _ -> xNoFlag -let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind +let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind (* New kinds of terms *) @@ -481,7 +481,7 @@ let input_term_annotation strm = | Tok.KEYWORD "@" :: _ -> `At | _ -> `None let term_annotation = - Gram.Entry.of_parser "term_annotation" input_term_annotation + Pcoq.Entry.of_parser "term_annotation" input_term_annotation (* terms *) @@ -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 @@ -800,7 +803,7 @@ let reject_ssrhid strm = | _ -> ()) | _ -> () -let test_nohidden = Pcoq.Gram.Entry.of_parser "test_ssrhid" reject_ssrhid +let test_nohidden = Pcoq.Entry.of_parser "test_ssrhid" reject_ssrhid } @@ -961,7 +964,7 @@ let accept_ssrfwdid strm = | Tok.IDENT id -> accept_before_syms_or_any_id [":"; ":="; "("] strm | _ -> raise Stream.Failure -let test_ssrfwdid = Gram.Entry.of_parser "test_ssrfwdid" accept_ssrfwdid +let test_ssrfwdid = Pcoq.Entry.of_parser "test_ssrfwdid" accept_ssrfwdid } @@ -1540,7 +1543,7 @@ let accept_ssrseqvar strm = accept_before_syms_or_ids ["["] ["first";"last"] strm | _ -> raise Stream.Failure -let test_ssrseqvar = Gram.Entry.of_parser "test_ssrseqvar" accept_ssrseqvar +let test_ssrseqvar = Pcoq.Entry.of_parser "test_ssrseqvar" accept_ssrseqvar let swaptacarg (loc, b) = (b, []), Some (TacId []) @@ -1605,14 +1608,14 @@ let old_tac = V82.tactic let ssr_reserved_ids = Summary.ref ~name:"SSR:idents" true -let _ = - Goptions.declare_bool_option - { Goptions.optname = "ssreflect identifiers"; - Goptions.optkey = ["SsrIdents"]; - Goptions.optdepr = false; - Goptions.optread = (fun _ -> !ssr_reserved_ids); - Goptions.optwrite = (fun b -> ssr_reserved_ids := b) - } +let () = + Goptions.(declare_bool_option + { optname = "ssreflect identifiers"; + optkey = ["SsrIdents"]; + optdepr = false; + optread = (fun _ -> !ssr_reserved_ids); + optwrite = (fun b -> ssr_reserved_ids := b) + }) let is_ssr_reserved s = let n = String.length s in n > 2 && s.[0] = '_' && s.[n - 1] = '_' @@ -1628,7 +1631,7 @@ let ssr_id_of_string loc s = ^ "Scripts with explicit references to anonymous variables are fragile.")) end; Id.of_string s -let ssr_null_entry = Gram.Entry.of_parser "ssr_null" (fun _ -> ()) +let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ -> ()) } @@ -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 @@ -1955,7 +1959,7 @@ let accept_ssreqid strm = accept_before_syms [":"] strm | _ -> raise Stream.Failure -let test_ssreqid = Gram.Entry.of_parser "test_ssreqid" accept_ssreqid +let test_ssreqid = Pcoq.Entry.of_parser "test_ssreqid" accept_ssreqid } @@ -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 @@ -2355,13 +2361,13 @@ END let ssr_rw_syntax = Summary.ref ~name:"SSR:rewrite" true -let _ = - Goptions.declare_bool_option - { Goptions.optname = "ssreflect rewrite"; - Goptions.optkey = ["SsrRewrite"]; - Goptions.optread = (fun _ -> !ssr_rw_syntax); - Goptions.optdepr = false; - Goptions.optwrite = (fun b -> ssr_rw_syntax := b) } +let () = + Goptions.(declare_bool_option + { optname = "ssreflect rewrite"; + optkey = ["SsrRewrite"]; + optread = (fun _ -> !ssr_rw_syntax); + optdepr = false; + optwrite = (fun b -> ssr_rw_syntax := b) }) let lbrace = Char.chr 123 (** Workaround to a limitation of coqpp *) @@ -2373,7 +2379,7 @@ let test_ssr_rw_syntax = match Util.stream_nth 0 strm with | Tok.KEYWORD key when List.mem key.[0] [lbrace; '['; '/'] -> () | _ -> raise Stream.Failure in - Gram.Entry.of_parser "test_ssr_rw_syntax" test + Pcoq.Entry.of_parser "test_ssr_rw_syntax" test } @@ -2583,7 +2589,7 @@ let accept_idcomma strm = | Tok.IDENT _ | Tok.KEYWORD "_" -> accept_before_syms [","] strm | _ -> raise Stream.Failure -let test_idcomma = Gram.Entry.of_parser "test_idcomma" accept_idcomma +let test_idcomma = Pcoq.Entry.of_parser "test_idcomma" accept_idcomma } 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/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 824666ba9c..8bf4816e99 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -119,13 +119,13 @@ and pr_iorpat iorpat = pr_list pr_bar pr_ipats iorpat (* 0 cost pp function. Active only if Debug Ssreflect is Set *) let ppdebug_ref = ref (fun _ -> ()) let ssr_pp s = Feedback.msg_debug (str"SSR: "++Lazy.force s) -let _ = - Goptions.declare_bool_option - { Goptions.optname = "ssreflect debugging"; - Goptions.optkey = ["Debug";"Ssreflect"]; - Goptions.optdepr = false; - Goptions.optread = (fun _ -> !ppdebug_ref == ssr_pp); - Goptions.optwrite = (fun b -> +let () = + Goptions.(declare_bool_option + { optname = "ssreflect debugging"; + optkey = ["Debug";"Ssreflect"]; + optdepr = false; + optread = (fun _ -> !ppdebug_ref == ssr_pp); + optwrite = (fun b -> Ssrmatching.debug b; - if b then ppdebug_ref := ssr_pp else ppdebug_ref := fun _ -> ()) } + if b then ppdebug_ref := ssr_pp else ppdebug_ref := fun _ -> ()) }) let ppdebug s = !ppdebug_ref s diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg index 3f0794fdd4..4ddaeb49fd 100644 --- a/plugins/ssrmatching/g_ssrmatching.mlg +++ b/plugins/ssrmatching/g_ssrmatching.mlg @@ -11,7 +11,6 @@ { open Ltac_plugin -open Pcoq open Pcoq.Constr open Ssrmatching open Ssrmatching.Internal @@ -69,7 +68,7 @@ let input_ssrtermkind strm = match Util.stream_nth 0 strm with | Tok.KEYWORD "(" -> '(' | Tok.KEYWORD "@" -> '@' | _ -> ' ' -let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind +let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind } diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 8cb0a8b463..6497b6ff98 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -896,7 +896,7 @@ let interp_rpattern s = function let interp_rpattern0 ist gl t = Tacmach.project gl, interp_rpattern ist t -type cpattern = char * glob_constr_and_expr * Geninterp.interp_sign option +type cpattern = char * Genintern.glob_constr_and_expr * Geninterp.interp_sign option let tag_of_cpattern = pi1 let loc_of_cpattern = loc_ofCG let cpattern_of_term (c, t) ist = c, t, Some ist diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 93a8c48435..8672c55767 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -5,9 +5,7 @@ open Goal open Environ open Evd open Constr - -open Ltac_plugin -open Tacexpr +open Genintern (** ******** Small Scale Reflection pattern matching facilities ************* *) |