aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/btauto/dune (renamed from plugins/btauto/plugin_base.dune)2
-rw-r--r--plugins/cc/ccalgo.ml17
-rw-r--r--plugins/cc/dune (renamed from plugins/cc/plugin_base.dune)2
-rw-r--r--plugins/derive/dune (renamed from plugins/derive/plugin_base.dune)2
-rw-r--r--plugins/extraction/dune (renamed from plugins/extraction/plugin_base.dune)2
-rw-r--r--plugins/extraction/table.ml39
-rw-r--r--plugins/firstorder/dune (renamed from plugins/firstorder/plugin_base.dune)2
-rw-r--r--plugins/firstorder/g_ground.mlg18
-rw-r--r--plugins/funind/dune (renamed from plugins/funind/plugin_base.dune)2
-rw-r--r--plugins/funind/gen_principle.ml71
-rw-r--r--plugins/funind/indfun_common.ml60
-rw-r--r--plugins/ltac/dune (renamed from plugins/ltac/plugin_base.dune)2
-rw-r--r--plugins/ltac/extratactics.mlg12
-rw-r--r--plugins/ltac/g_auto.mlg2
-rw-r--r--plugins/ltac/g_ltac.mlg12
-rw-r--r--plugins/ltac/tacentries.ml54
-rw-r--r--plugins/ltac/tacenv.ml2
-rw-r--r--plugins/ltac/tacinterp.ml8
-rw-r--r--plugins/ltac/tactic_option.ml11
-rw-r--r--plugins/micromega/.ocamlformat1
-rw-r--r--plugins/micromega/.ocamlformat-ignore1
-rw-r--r--plugins/micromega/certificate.ml20
-rw-r--r--plugins/micromega/certificate.mli6
-rw-r--r--plugins/micromega/coq_micromega.ml91
-rw-r--r--plugins/micromega/dune (renamed from plugins/micromega/plugin_base.dune)2
-rw-r--r--plugins/micromega/persistent_cache.ml46
-rw-r--r--plugins/nsatz/dune (renamed from plugins/nsatz/plugin_base.dune)2
-rw-r--r--plugins/omega/dune (renamed from plugins/omega/plugin_base.dune)2
-rw-r--r--plugins/rtauto/dune (renamed from plugins/rtauto/plugin_base.dune)2
-rw-r--r--plugins/rtauto/proof_search.ml18
-rw-r--r--plugins/rtauto/refl_tauto.ml44
-rw-r--r--plugins/setoid_ring/dune (renamed from plugins/setoid_ring/plugin_base.dune)2
-rw-r--r--plugins/ssr/dune (renamed from plugins/ssr/plugin_base.dune)2
-rw-r--r--plugins/ssr/ssrcommon.ml2
-rw-r--r--plugins/ssr/ssrvernac.mlg2
-rw-r--r--plugins/ssrmatching/dune (renamed from plugins/ssrmatching/plugin_base.dune)2
-rw-r--r--plugins/syntax/dune (renamed from plugins/syntax/plugin_base.dune)2
-rw-r--r--plugins/syntax/float_syntax.ml50
38 files changed, 290 insertions, 327 deletions
diff --git a/plugins/btauto/plugin_base.dune b/plugins/btauto/dune
index 6a024358c3..d2f5b65980 100644
--- a/plugins/btauto/plugin_base.dune
+++ b/plugins/btauto/dune
@@ -3,3 +3,5 @@
(public_name coq.plugins.btauto)
(synopsis "Coq's btauto plugin")
(libraries coq.plugins.ltac))
+
+(coq.pp (modules g_btauto))
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 74043d6bc8..6f5c910297 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -25,19 +25,14 @@ open Util
let init_size=5
-let cc_verbose=ref false
+let cc_verbose=
+ declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Congruence";"Verbose"]
+ ~value:false
let debug x =
- if !cc_verbose then Feedback.msg_debug (x ())
-
-let () =
- let gdopt=
- { optdepr=false;
- optkey=["Congruence";"Verbose"];
- optread=(fun ()-> !cc_verbose);
- optwrite=(fun b -> cc_verbose := b)}
- in
- declare_bool_option gdopt
+ if cc_verbose () then Feedback.msg_debug (x ())
(* Signature table *)
diff --git a/plugins/cc/plugin_base.dune b/plugins/cc/dune
index 2a92996d2a..f7fa3adb56 100644
--- a/plugins/cc/plugin_base.dune
+++ b/plugins/cc/dune
@@ -3,3 +3,5 @@
(public_name coq.plugins.cc)
(synopsis "Coq's congruence closure plugin")
(libraries coq.plugins.ltac))
+
+(coq.pp (modules g_congruence))
diff --git a/plugins/derive/plugin_base.dune b/plugins/derive/dune
index ba9cd595ce..1931339471 100644
--- a/plugins/derive/plugin_base.dune
+++ b/plugins/derive/dune
@@ -3,3 +3,5 @@
(public_name coq.plugins.derive)
(synopsis "Coq's derive plugin")
(libraries coq.plugins.ltac))
+
+(coq.pp (modules g_derive))
diff --git a/plugins/extraction/plugin_base.dune b/plugins/extraction/dune
index 037b0d5053..0c01dcd488 100644
--- a/plugins/extraction/plugin_base.dune
+++ b/plugins/extraction/dune
@@ -3,3 +3,5 @@
(public_name coq.plugins.extraction)
(synopsis "Coq's extraction plugin")
(libraries num coq.plugins.ltac))
+
+(coq.pp (modules g_extraction))
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index a53c2395f0..f8449bcda1 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -498,16 +498,8 @@ let info_file f =
(* The objects defined below should survive an arbitrary time,
so we register them to coq save/undo mechanism. *)
-let my_bool_option name initval =
- let flag = ref initval in
- let access = fun () -> !flag in
- let () = declare_bool_option
- {optdepr = false;
- optkey = ["Extraction"; name];
- optread = access;
- optwrite = (:=) flag }
- in
- access
+let my_bool_option name value =
+ declare_bool_option_and_ref ~depr:false ~key:["Extraction"; name] ~value
(*s Extraction AccessOpaque *)
@@ -588,25 +580,18 @@ let () = declare_int_option
(* This option controls whether "dummy lambda" are removed when a
toplevel constant is defined. *)
-let conservative_types_ref = ref false
-let conservative_types () = !conservative_types_ref
-
-let () = declare_bool_option
- {optdepr = false;
- optkey = ["Extraction"; "Conservative"; "Types"];
- optread = (fun () -> !conservative_types_ref);
- optwrite = (fun b -> conservative_types_ref := b) }
-
+let conservative_types =
+ declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Extraction"; "Conservative"; "Types"]
+ ~value:false
(* Allows to print a comment at the beginning of the output files *)
-let file_comment_ref = ref ""
-let file_comment () = !file_comment_ref
-
-let () = declare_string_option
- {optdepr = false;
- optkey = ["Extraction"; "File"; "Comment"];
- optread = (fun () -> !file_comment_ref);
- optwrite = (fun s -> file_comment_ref := s) }
+let file_comment =
+ declare_string_option_and_ref
+ ~depr:false
+ ~key:["Extraction"; "File"; "Comment"]
+ ~value:""
(*s Extraction Lang *)
diff --git a/plugins/firstorder/plugin_base.dune b/plugins/firstorder/dune
index d88daa23fc..1b05452d8f 100644
--- a/plugins/firstorder/plugin_base.dune
+++ b/plugins/firstorder/dune
@@ -3,3 +3,5 @@
(public_name coq.plugins.firstorder)
(synopsis "Coq's first order logic solver plugin")
(libraries coq.plugins.ltac))
+
+(coq.pp (modules g_ground))
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 49e4c91182..6ddc6ba21e 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -31,20 +31,8 @@ DECLARE PLUGIN "ground_plugin"
{
-let ground_depth=ref 3
-
-let ()=
- let gdopt=
- { optdepr=false;
- optkey=["Firstorder";"Depth"];
- optread=(fun ()->Some !ground_depth);
- optwrite=
- (function
- None->ground_depth:=3
- | Some i->ground_depth:=(max i 0))}
- in
- declare_int_option gdopt
-
+let ground_depth =
+ declare_nat_option_and_ref ~depr:false ~key:["Firstorder";"Depth"] ~value:3
let default_intuition_tac =
let tac _ _ = Auto.h_auto None [] (Some []) in
@@ -85,7 +73,7 @@ let gen_ground_tac flag taco ids bases =
| None-> snd (default_solver ()) in
let startseq k =
Proofview.Goal.enter begin fun gl ->
- let seq=empty_seq !ground_depth in
+ let seq=empty_seq (ground_depth ()) in
let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in
let seq, sigma = extend_with_auto_hints (pf_env gl) sigma bases seq in
tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq)
diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/dune
index 6ccf15df29..e594ffbd02 100644
--- a/plugins/funind/plugin_base.dune
+++ b/plugins/funind/dune
@@ -3,3 +3,5 @@
(public_name coq.plugins.funind)
(synopsis "Coq's functional induction plugin")
(libraries coq.plugins.extraction))
+
+(coq.pp (modules g_indfun))
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 446026c4c8..d38c3c869b 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -39,7 +39,7 @@ let build_newrecursive lnameargsardef =
List.fold_left
(fun (env,impls) { Vernacexpr.fname={CAst.v=recname}; binders; rtype } ->
let arityc = Constrexpr_ops.mkCProdN binders rtype in
- let arity,ctx = Constrintern.interp_type env0 sigma arityc in
+ let arity,_ctx = Constrintern.interp_type env0 sigma arityc in
let evd = Evd.from_env env0 in
let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd binders in
let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in
@@ -164,7 +164,7 @@ let prepare_body { Vernacexpr.binders } rt =
let fun_args,rt' = chop_rlambda_n n rt in
(fun_args,rt')
-let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook =
+let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_map ref) old_princ_type sorts funs _i proof_tac hook =
(* First we get the type of the old graph principle *)
let mutr_nparams = (Tactics.compute_elim_sig !evd (EConstr.of_constr old_princ_type)).Tactics.nparams in
(* let time1 = System.get_time () in *)
@@ -199,7 +199,7 @@ let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_
(* end; *)
let open Proof_global in
- let { name; entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in
+ let { entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false) lemma in
match entries with
| [entry] ->
entry, hook
@@ -235,7 +235,6 @@ let change_property_sort evd toSort princ princName =
(List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_info.Tactics.params)
let generate_functional_principle (evd: Evd.evar_map ref)
- interactive_proof
old_princ_type sorts new_princ_name funs i proof_tac
=
try
@@ -283,27 +282,25 @@ let generate_functional_principle (evd: Evd.evar_map ref)
register_with_sort Sorts.InSet
in
let entry, hook =
- build_functional_principle evd interactive_proof old_princ_type new_sorts funs i
+ build_functional_principle evd old_princ_type new_sorts funs i
proof_tac hook
in
(* Pr 1278 :
Don't forget to close the goal if an error is raised !!!!
*)
let uctx = Evd.evar_universe_context sigma in
- let hook_data = hook, uctx, [] in
- let _ : Names.GlobRef.t = DeclareDef.declare_definition
- ~name:new_princ_name ~hook_data
+ let _ : Names.GlobRef.t = DeclareDef.declare_entry
+ ~name:new_princ_name ~hook
~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
~kind:Decls.(IsProof Theorem)
- ~ubind:UnivNames.empty_binders
~impargs:[]
- entry in
+ ~uctx entry in
()
with e when CErrors.noncritical e ->
raise (Defining_principle e)
let generate_principle (evd:Evd.evar_map ref) pconstants on_error
- is_general do_built fix_rec_l recdefs interactive_proof
+ is_general do_built fix_rec_l recdefs
(continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int ->
Tacmach.tactic) : unit =
let names = List.map (function { Vernacexpr.fname = {CAst.v=name} } -> name) fix_rec_l in
@@ -336,7 +333,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in
let _ =
List.map_i
- (fun i x ->
+ (fun i _x ->
let env = Global.env () in
let princ = Indrec.lookup_eliminator env (ind_kn,i) (Sorts.InProp) in
let evd = ref (Evd.from_env env) in
@@ -347,7 +344,6 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
let princ_type = EConstr.Unsafe.to_constr princ_type in
generate_functional_principle
evd
- interactive_proof
princ_type
None
None
@@ -375,7 +371,6 @@ let register_struct is_rec fixpoint_exprl =
| None ->
CErrors.user_err ~hdr:"Function" Pp.(str "Body of Function must be given") in
ComDefinition.do_definition
- ~program_mode:false
~name:fname.CAst.v
~poly:false
~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
@@ -413,7 +408,7 @@ let register_struct is_rec fixpoint_exprl =
None,evd,List.rev rev_pconstants
let generate_correction_proof_wf f_ref tcc_lemma_ref
- is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
+ is_mes functional_ref eq_ref rec_arg_num rec_arg_type relation
(_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Tacmach.tactic =
Functional_principles_proofs.prove_principle_for_gen
(f_ref,functional_ref,eq_ref)
@@ -431,7 +426,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref
res = fv \rightarrow graph\ x_1\ldots x_n\ res\] decomposed as the context and the conclusion
*)
-let generate_type evd g_to_f f graph i =
+let generate_type evd g_to_f f graph =
let open Context.Rel.Declaration in
let open EConstr in
let open EConstr.Vars in
@@ -499,7 +494,7 @@ let generate_type evd g_to_f f graph i =
WARNING: while convertible, [type_of body] and [type] can be non equal
*)
let find_induction_principle evd f =
- let f_as_constant,u = match EConstr.kind !evd f with
+ let f_as_constant, _u = match EConstr.kind !evd f with
| Constr.Const c' -> c'
| _ -> CErrors.user_err Pp.(str "Must be used with a function")
in
@@ -546,7 +541,7 @@ let rec generate_fresh_id x avoid i =
let id = Namegen.next_ident_away_in_goal x (Id.Set.of_list avoid) in
id::(generate_fresh_id x (id::avoid) (pred i))
-let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic =
+let prove_fun_correct evd graphs_constr schemes lemmas_types_infos i : Tacmach.tactic =
let open Constr in
let open EConstr in
let open Context.Rel.Declaration in
@@ -1141,7 +1136,7 @@ let get_funs_constant mp =
to prevent Reset strange thing
*)
let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in
- let l_params,l_fixes = List.split (List.map Term.decompose_lam l_bodies) in
+ let l_params, _l_fixes = List.split (List.map Term.decompose_lam l_bodies) in
(* all the parameters must be equal*)
let _check_params =
let first_params = List.hd l_params in
@@ -1241,7 +1236,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
in
let entry, _hook =
try
- build_functional_principle ~opaque evd false
+ build_functional_principle ~opaque evd
first_type
(Array.of_list sorts)
this_block_funs
@@ -1262,7 +1257,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
let sorts = Array.of_list sorts in
List.map (Functional_principles_types.compute_new_princ_type_from_rel funs sorts) other_princ_types
in
- let first_princ_body,first_princ_type = Declare.(entry.proof_entry_body, entry.proof_entry_type) in
+ let first_princ_body = entry.Declare.proof_entry_body in
let ctxt,fix = Term.decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
let (idxs,_),(_,ta,_ as decl) = Constr.destFix fix in
let other_result =
@@ -1292,7 +1287,6 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
let entry, _hook =
build_functional_principle
evd
- false
(List.nth other_princ_types (!i - 1))
(Array.of_list sorts)
this_block_funs
@@ -1331,9 +1325,8 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
let lemmas_types_infos =
Util.Array.map2_i
(fun i f_constr graph ->
- (* let const_of_f,u = destConst f_constr in *)
let (type_of_lemma_ctxt,type_of_lemma_concl,graph) =
- generate_type evd false f_constr graph i
+ generate_type evd false f_constr graph
in
let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
graphs_constr.(i) <- graph;
@@ -1368,7 +1361,7 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
)
in
let proving_tac =
- prove_fun_correct !evd funs_constr graphs_constr schemes lemmas_types_infos
+ prove_fun_correct !evd graphs_constr schemes lemmas_types_infos
in
Array.iteri
(fun i f_as_constant ->
@@ -1398,8 +1391,8 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
let lemmas_types_infos =
Util.Array.map2_i
(fun i f_constr graph ->
- let (type_of_lemma_ctxt,type_of_lemma_concl,graph) =
- generate_type evd true f_constr graph i
+ let (type_of_lemma_ctxt,type_of_lemma_concl,graph) =
+ generate_type evd true f_constr graph
in
let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
graphs_constr.(i) <- graph;
@@ -1415,7 +1408,7 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
in
let (kn,_) as graph_ind,u = (destInd !evd graphs_constr.(0)) in
- let mib,mip = Global.lookup_inductive graph_ind in
+ let mib, _mip = Global.lookup_inductive graph_ind in
let sigma, scheme =
(Indrec.build_mutual_induction_scheme (Global.env ()) !evd
(Array.to_list
@@ -1485,7 +1478,7 @@ let derive_inversion fix_names =
*)
List.iter (fun c -> ignore (find_Function_infos (fst c))) fix_names_as_constant ;
try
- let evd', lind =
+ let _evd', lind =
List.fold_right
(fun id (evd,l) ->
let evd,id =
@@ -1536,11 +1529,11 @@ let register_wf interactive_proof ?(is_mes=false) fname rec_impls wf_rel_expr wf
in
let eq = Constrexpr_ops.mkCProdN args unbounded_eq in
let hook ((f_ref,_) as fconst) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type
- nb_args relation =
+ _nb_args relation =
try
pre_hook [fconst]
(generate_correction_proof_wf f_ref tcc_lemma_ref is_mes
- functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
+ functional_ref eq_ref rec_arg_num rec_arg_type relation
);
derive_inversion [fname]
with e when CErrors.noncritical e ->
@@ -1562,7 +1555,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt w
| None ->
begin
match args with
- | [Constrexpr.CLocalAssum ([{CAst.v=Name x}],k,t)] -> t,x
+ | [Constrexpr.CLocalAssum ([{CAst.v=Name x}],_k,t)] -> t,x
| _ -> CErrors.user_err (Pp.str "Recursive argument must be specified")
end
| Some wf_args ->
@@ -1570,7 +1563,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt w
match
List.find
(function
- | Constrexpr.CLocalAssum(l,k,t) ->
+ | Constrexpr.CLocalAssum(l,_k,t) ->
List.exists
(function {CAst.v=Name id} -> Id.equal id wf_args | _ -> false)
l
@@ -1578,7 +1571,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt w
)
args
with
- | Constrexpr.CLocalAssum(_,k,t) -> t,wf_args
+ | Constrexpr.CLocalAssum(_,_k,t) -> t,wf_args
| _ -> assert false
with Not_found -> assert false
in
@@ -1626,7 +1619,7 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
let lemma, _is_struct =
match fixpoint_exprl with
| [{ Vernacexpr.rec_order = Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)} } as fixpoint_expr] ->
- let { Vernacexpr.fname; univs; binders; rtype; body_def } as fixpoint_expr =
+ let { Vernacexpr.fname; univs = _; binders; rtype; body_def } as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
| _ -> assert false
@@ -1645,13 +1638,12 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
register_built
fixpoint_exprl
recdefs
- true
in
if register_built
then register_wf interactive_proof fname.CAst.v rec_impls wf_rel wf_x.CAst.v using_lemmas binders rtype body pre_hook, false
else None, false
| [{ Vernacexpr.rec_order = Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)} } as fixpoint_expr] ->
- let { Vernacexpr.fname; univs; binders; rtype; body_def} as fixpoint_expr =
+ let { Vernacexpr.fname; univs = _; binders; rtype; body_def} as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
| _ -> assert false
@@ -1672,7 +1664,6 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
register_built
fixpoint_exprl
recdefs
- true
in
if register_built
then register_mes interactive_proof fname.CAst.v rec_impls wf_mes wf_rel_opt
@@ -1690,7 +1681,7 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
let fixpoint_exprl = recompute_binder_list fixpoint_exprl in
let fix_names = List.map (function { Vernacexpr.fname } -> fname.CAst.v) fixpoint_exprl in
(* ok all the expressions are structural *)
- let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
+ let recdefs, _rec_impls = build_newrecursive fixpoint_exprl in
let is_rec = List.exists (is_rec fix_names) recdefs in
let lemma,evd,pconstants =
if register_built
@@ -1706,7 +1697,6 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
register_built
fixpoint_exprl
recdefs
- interactive_proof
(Functional_principles_proofs.prove_princ_for_struct evd interactive_proof);
if register_built then
begin derive_inversion fix_names; end;
@@ -2067,7 +2057,6 @@ let build_case_scheme fa =
*)
generate_functional_principle
(ref (Evd.from_env (Global.env ())))
- false
scheme_type
(Some ([|sorts|]))
(Some princ_name)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 7d87fc0220..ec23355ce1 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -107,9 +107,9 @@ let with_full_print f a =
and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
let old_rawprint = !Flags.raw_print in
let old_printuniverses = !Constrextern.print_universes in
- let old_printallowmatchdefaultclause = !Detyping.print_allow_match_default_clause in
+ let old_printallowmatchdefaultclause = Detyping.print_allow_match_default_clause () in
Constrextern.print_universes := true;
- Detyping.print_allow_match_default_clause := false;
+ Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name false;
Flags.raw_print := true;
Impargs.make_implicit_args false;
Impargs.make_strict_implicit_args false;
@@ -122,7 +122,7 @@ let with_full_print f a =
Impargs.make_contextual_implicit_args old_contextual_implicit_args;
Flags.raw_print := old_rawprint;
Constrextern.print_universes := old_printuniverses;
- Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause;
+ Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name old_printallowmatchdefaultclause;
Dumpglob.continue ();
res
with
@@ -132,7 +132,7 @@ let with_full_print f a =
Impargs.make_contextual_implicit_args old_contextual_implicit_args;
Flags.raw_print := old_rawprint;
Constrextern.print_universes := old_printuniverses;
- Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause;
+ Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name old_printallowmatchdefaultclause;
Dumpglob.continue ();
raise reraise
@@ -309,33 +309,18 @@ let add_Function is_general f =
let pr_table env sigma = pr_table env sigma !from_function
(*********************************)
(* Debugging *)
-let functional_induction_rewrite_dependent_proofs = ref true
-let function_debug = ref false
-open Goptions
-let functional_induction_rewrite_dependent_proofs_sig =
- {
- optdepr = false;
- optkey = ["Functional";"Induction";"Rewrite";"Dependent"];
- 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 do_rewrite_dependent =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Functional";"Induction";"Rewrite";"Dependent"]
+ ~value:true
-let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = true
-
-let function_debug_sig =
- {
- optdepr = false;
- optkey = ["Function_debug"];
- optread = (fun () -> !function_debug);
- optwrite = (fun b -> function_debug := b)
- }
-
-let () = declare_bool_option function_debug_sig
-
-
-let do_observe () = !function_debug
+let do_observe =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Function_debug"]
+ ~value:false
let observe strm =
if do_observe ()
@@ -405,18 +390,11 @@ let observe_tac ~header s tac =
end
-let strict_tcc = ref false
-let is_strict_tcc () = !strict_tcc
-let strict_tcc_sig =
- {
- optdepr = false;
- optkey = ["Function_raw_tcc"];
- optread = (fun () -> !strict_tcc);
- optwrite = (fun b -> strict_tcc := b)
- }
-
-let () = declare_bool_option strict_tcc_sig
-
+let is_strict_tcc =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Function_raw_tcc"]
+ ~value:false
exception Building_graph of exn
exception Defining_principle of exn
diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/dune
index 5611f5ba16..6558ecbfe8 100644
--- a/plugins/ltac/plugin_base.dune
+++ b/plugins/ltac/dune
@@ -11,3 +11,5 @@
(synopsis "Coq's tauto tactic")
(modules tauto)
(libraries coq.plugins.ltac))
+
+(coq.pp (modules extratactics g_tactic g_rewrite g_eqdecide g_auto g_obligations g_ltac profile_ltac_tactics coretactics g_class extraargs))
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 9b80cbd803..7b1aa7a07a 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -47,7 +47,7 @@ DECLARE PLUGIN "ltac_plugin"
let with_delayed_uconstr ist c tac =
let flags = {
- Pretyping.use_typeclasses = false;
+ Pretyping.use_typeclasses = Pretyping.NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
@@ -345,7 +345,7 @@ open EConstr
open Vars
let constr_flags () = {
- Pretyping.use_typeclasses = true;
+ Pretyping.use_typeclasses = Pretyping.UseTC;
Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics ();
Pretyping.fail_evar = false;
Pretyping.expand_evars = true;
@@ -375,22 +375,22 @@ let refine_tac ist simple with_classes c =
TACTIC EXTEND refine
| [ "refine" uconstr(c) ] ->
- { refine_tac ist false true c }
+ { refine_tac ist false Pretyping.UseTC c }
END
TACTIC EXTEND simple_refine
| [ "simple" "refine" uconstr(c) ] ->
- { refine_tac ist true true c }
+ { refine_tac ist true Pretyping.UseTC c }
END
TACTIC EXTEND notcs_refine
| [ "notypeclasses" "refine" uconstr(c) ] ->
- { refine_tac ist false false c }
+ { refine_tac ist false Pretyping.NoUseTC c }
END
TACTIC EXTEND notcs_simple_refine
| [ "simple" "notypeclasses" "refine" uconstr(c) ] ->
- { refine_tac ist true false c }
+ { refine_tac ist true Pretyping.NoUseTC c }
END
(* Solve unification constraints using heuristics or fail if any remain *)
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 3c30c881fb..b4527694ae 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -53,7 +53,7 @@ END
let eval_uconstrs ist cs =
let flags = {
- Pretyping.use_typeclasses = false;
+ Pretyping.use_typeclasses = Pretyping.NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 50c3ed1248..2bd4211c90 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -359,21 +359,15 @@ open Vernacextend
open Goptions
open Libnames
-let print_info_trace = ref None
-
-let () = declare_int_option {
- optdepr = false;
- optkey = ["Info" ; "Level"];
- optread = (fun () -> !print_info_trace);
- optwrite = fun n -> print_info_trace := n;
-}
+let print_info_trace =
+ declare_intopt_option_and_ref ~depr:false ~key:["Info" ; "Level"]
let vernac_solve ~pstate n info tcom b =
let open Goal_select in
let pstate, status = Proof_global.map_fold_proof_endline (fun etac p ->
let with_end_tac = if b then Some etac else None in
let global = match n with SelectAll | SelectList _ -> true | _ -> false in
- let info = Option.append info !print_info_trace in
+ let info = Option.append info (print_info_trace ()) in
let (p,status) =
Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
in
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 4af5699317..9910796d9c 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -44,11 +44,11 @@ let coincide s pat off =
!break
let atactic n =
- if n = 5 then Aentry Pltac.binder_tactic
- else Aentryl (Pltac.tactic_expr, string_of_int n)
+ if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic
+ else Pcoq.Symbol.nterml Pltac.tactic_expr (string_of_int n)
type entry_name = EntryName :
- 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Extend.symbol -> entry_name
+ 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.Symbol.t -> entry_name
(** Quite ad-hoc *)
let get_tacentry n m =
@@ -57,8 +57,8 @@ let get_tacentry n m =
&& not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
&& not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
in
- if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Aself)
- else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Anext)
+ if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Pcoq.Symbol.self)
+ else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Pcoq.Symbol.next)
else EntryName (rawwit Tacarg.wit_tactic, atactic n)
let get_separator = function
@@ -140,23 +140,23 @@ let head_is_ident tg = match tg.tacgram_prods with
let rec prod_item_of_symbol lev = function
| Extend.Ulist1 s ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (ListArg typ), Alist1 e)
+ EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list1 e)
| Extend.Ulist0 s ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (ListArg typ), Alist0 e)
+ EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list0 e)
| Extend.Ulist1sep (s, sep) ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (ListArg typ), Alist1sep (e, Atoken (CLexer.terminal sep)))
+ EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list1sep e (Pcoq.Symbol.token (CLexer.terminal sep)) false)
| Extend.Ulist0sep (s, sep) ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (ListArg typ), Alist0sep (e, Atoken (CLexer.terminal sep)))
+ EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list0sep e (Pcoq.Symbol.token (CLexer.terminal sep)) false)
| Extend.Uopt s ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (OptArg typ), Aopt e)
+ EntryName (Rawwit (OptArg typ), Pcoq.Symbol.opt e)
| Extend.Uentry arg ->
let ArgT.Any tag = arg in
let wit = ExtraArg tag in
- EntryName (Rawwit wit, Extend.Aentry (genarg_grammar wit))
+ EntryName (Rawwit wit, Pcoq.Symbol.nterm (genarg_grammar wit))
| Extend.Uentryl (s, n) ->
let ArgT.Any tag = s in
assert (coincide (ArgT.repr tag) "tactic" 0);
@@ -191,7 +191,7 @@ let add_tactic_entry (kn, ml, tg) state =
in
let prods = List.map map tg.tacgram_prods in
let rules = make_rule mkact prods in
- let r = ExtendRule (entry, (pos, [(None, None, [rules])])) in
+ let r = ExtendRule (entry, { pos; data=[(None, None, [rules])]}) in
([r], state)
let tactic_grammar =
@@ -299,7 +299,7 @@ let classify_tactic_notation tacobj = Substitute tacobj
let inTacticGrammar : tactic_grammar_obj -> obj =
declare_object {(default_object "TacticGrammar") with
- open_function = open_tactic_notation;
+ open_function = simple_open open_tactic_notation;
load_function = load_tactic_notation;
cache_function = cache_tactic_notation;
subst_function = subst_tactic_notation;
@@ -399,23 +399,29 @@ let create_ltac_quotation name cast (e, l) =
in
let () = ltac_quotations := String.Set.add name !ltac_quotations in
let entry = match l with
- | None -> Aentry e
- | Some l -> Aentryl (e, string_of_int l)
+ | None -> Pcoq.Symbol.nterm e
+ | Some l -> Pcoq.Symbol.nterml e (string_of_int l)
in
(* let level = Some "1" in *)
let level = None in
let assoc = None in
let rule =
- Next (Next (Next (Next (Next (Stop,
- Atoken (CLexer.terminal name)),
- Atoken (CLexer.terminal ":")),
- Atoken (CLexer.terminal "(")),
- entry),
- Atoken (CLexer.terminal ")"))
+ Pcoq.(
+ Rule.next
+ (Rule.next
+ (Rule.next
+ (Rule.next
+ (Rule.next
+ Rule.stop
+ (Symbol.token (CLexer.terminal name)))
+ (Symbol.token (CLexer.terminal ":")))
+ (Symbol.token (CLexer.terminal "(")))
+ entry)
+ (Symbol.token (CLexer.terminal ")")))
in
let action _ v _ _ _ loc = cast (Some loc, v) in
- let gram = (level, assoc, [Rule (rule, action)]) in
- Pcoq.grammar_extend Pltac.tactic_arg (None, [gram])
+ let gram = (level, assoc, [Pcoq.Production.make rule action]) in
+ Pcoq.grammar_extend Pltac.tactic_arg {pos=None; data=[gram]}
(** Command *)
@@ -759,7 +765,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) =
e
| Vernacextend.Arg_rules rules ->
let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
- let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in
+ let () = Pcoq.grammar_extend e {pos=None; data=[(None, None, rules)]} in
e
in
let (rpr, gpr, tpr) = arg.arg_printer in
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index ce9189792e..76d47f5482 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -182,7 +182,7 @@ let inMD : bool * ltac_constant option * bool * glob_tactic_expr *
declare_object {(default_object "TAC-DEFINITION") with
cache_function = cache_md;
load_function = load_md;
- open_function = open_md;
+ open_function = simple_open open_md;
subst_function = subst_md;
classify_function = classify_md}
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 9e0b9d3254..b0e26e1def 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -546,7 +546,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
(evd,c)
let constr_flags () = {
- use_typeclasses = true;
+ use_typeclasses = UseTC;
solve_unification_constraints = true;
fail_evar = true;
expand_evars = true;
@@ -564,7 +564,7 @@ let interp_constr = interp_constr_gen WithoutTypeConstraint
let interp_type = interp_constr_gen IsType
let open_constr_use_classes_flags () = {
- use_typeclasses = true;
+ use_typeclasses = UseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
@@ -573,7 +573,7 @@ let open_constr_use_classes_flags () = {
}
let open_constr_no_classes_flags () = {
- use_typeclasses = false;
+ use_typeclasses = NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
@@ -582,7 +582,7 @@ let open_constr_no_classes_flags () = {
}
let pure_open_constr_flags = {
- use_typeclasses = false;
+ use_typeclasses = NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = false;
diff --git a/plugins/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml
index c72a527537..922d2f7792 100644
--- a/plugins/ltac/tactic_option.ml
+++ b/plugins/ltac/tactic_option.ml
@@ -13,15 +13,11 @@ open Pp
let declare_tactic_option ?(default=Tacexpr.TacId []) name =
let locality = Summary.ref false ~name:(name^"-locality") in
- let default_tactic_expr : Tacexpr.glob_tactic_expr ref =
- Summary.ref default ~name:(name^"-default-tacexpr")
- in
let default_tactic : Tacexpr.glob_tactic_expr ref =
- Summary.ref !default_tactic_expr ~name:(name^"-default-tactic")
+ Summary.ref default ~name:(name^"-default-tactic")
in
let set_default_tactic local t =
locality := local;
- default_tactic_expr := t;
default_tactic := t
in
let cache (_, (local, tac)) = set_default_tactic local tac in
@@ -36,18 +32,17 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name =
{ (default_object name) with
cache_function = cache;
load_function = (fun _ -> load);
- open_function = (fun _ -> load);
+ open_function = simple_open (fun _ -> load);
classify_function = (fun (local, tac) ->
if local then Dispose else Substitute (local, tac));
subst_function = subst}
in
let put local tac =
- set_default_tactic local tac;
Lib.add_anonymous_leaf (input (local, tac))
in
let get () = !locality, Tacinterp.eval_tactic !default_tactic in
let print () =
- Pptactic.pr_glob_tactic (Global.env ()) !default_tactic_expr ++
+ Pptactic.pr_glob_tactic (Global.env ()) !default_tactic ++
(if !locality then str" (locally defined)" else str" (globally defined)")
in
put, get, print
diff --git a/plugins/micromega/.ocamlformat b/plugins/micromega/.ocamlformat
new file mode 100644
index 0000000000..a22a2ff88c
--- /dev/null
+++ b/plugins/micromega/.ocamlformat
@@ -0,0 +1 @@
+disable=false
diff --git a/plugins/micromega/.ocamlformat-ignore b/plugins/micromega/.ocamlformat-ignore
new file mode 100644
index 0000000000..157a987754
--- /dev/null
+++ b/plugins/micromega/.ocamlformat-ignore
@@ -0,0 +1 @@
+micromega.ml
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 1958fff4cc..9eeba614c7 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -27,7 +27,13 @@ open NumCompat
open Q.Notations
open Mutils
-let use_simplex = ref true
+let use_simplex =
+ Goptions.declare_bool_option_and_ref ~depr:false ~key:["Simplex"] ~value:true
+
+(* If set to some [file], arithmetic goals are dumped in [file].v *)
+
+let dump_file =
+ Goptions.declare_stringopt_option_and_ref ~depr:false ~key:["Dump"; "Arith"]
type ('prf, 'model) res = Prf of 'prf | Model of 'model | Unknown
type zres = (Mc.zArithProof, int * Mc.z list) res
@@ -203,19 +209,19 @@ let fourier_linear_prover l =
| Inl _ -> None
let direct_linear_prover l =
- if !use_simplex then Simplex.find_unsat_certificate l
+ if use_simplex () then Simplex.find_unsat_certificate l
else fourier_linear_prover l
let find_point l =
let open Util in
- if !use_simplex then Simplex.find_point l
+ if use_simplex () then Simplex.find_point l
else
match Mfourier.Fourier.find_point l with
| Inr _ -> None
| Inl cert -> Some cert
let optimise v l =
- if !use_simplex then Simplex.optimise v l else Mfourier.Fourier.optimise v l
+ if use_simplex () then Simplex.optimise v l else Mfourier.Fourier.optimise v l
let dual_raw_certificate l =
if debug then begin
@@ -981,13 +987,11 @@ let xlia_simplex env red sys =
with FoundProof prf -> compile_prf sys (Step (0, prf, Done))
let xlia env0 en red sys =
- if !use_simplex then xlia_simplex env0 red sys else xlia en red sys
-
-let dump_file = ref None
+ if use_simplex () then xlia_simplex env0 red sys else xlia en red sys
let gen_bench (tac, prover) can_enum prfdepth sys =
let res = prover can_enum prfdepth sys in
- ( match !dump_file with
+ ( match dump_file () with
| None -> ()
| Some file ->
let o = open_out (Filename.temp_file ~temp_dir:(Sys.getcwd ()) file ".v") in
diff --git a/plugins/micromega/certificate.mli b/plugins/micromega/certificate.mli
index cabd36ebb7..5b215549b0 100644
--- a/plugins/micromega/certificate.mli
+++ b/plugins/micromega/certificate.mli
@@ -12,16 +12,12 @@ module Mc = Micromega
(** [use_simplex] is bound to the Coq option Simplex.
If set, use the Simplex method, otherwise use Fourier *)
-val use_simplex : bool ref
+val use_simplex : unit -> bool
type ('prf, 'model) res = Prf of 'prf | Model of 'model | Unknown
type zres = (Mc.zArithProof, int * Mc.z list) res
type qres = (Mc.q Mc.psatz, int * Mc.q list) res
-(** [dump_file] is bound to the Coq option Dump Arith.
- If set to some [file], arithmetic goals are dumped in filexxx.v *)
-val dump_file : string option ref
-
(** [q_cert_of_pos prf] converts a Sos proof into a rational Coq proof *)
val q_cert_of_pos : Sos_types.positivstellensatz -> Mc.q Mc.psatz
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 43f6f5a35e..7e4c4ce5c6 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -37,74 +37,31 @@ let debug = false
let max_depth = max_int
(* Search limit for provers over Q R *)
-let lra_proof_depth = ref max_depth
+let lra_proof_depth =
+ declare_int_option_and_ref ~depr:false ~key:["Lra"; "Depth"] ~value:max_depth
(* Search limit for provers over Z *)
-let lia_enum = ref true
-let lia_proof_depth = ref max_depth
-let get_lia_option () = (!Certificate.use_simplex, !lia_enum, !lia_proof_depth)
-let get_lra_option () = !lra_proof_depth
+let lia_enum =
+ declare_bool_option_and_ref ~depr:false ~key:["Lia"; "Enum"] ~value:true
+
+let lia_proof_depth =
+ declare_int_option_and_ref ~depr:false ~key:["Lia"; "Depth"] ~value:max_depth
+
+let get_lia_option () =
+ (Certificate.use_simplex (), lia_enum (), lia_proof_depth ())
(* Enable/disable caches *)
-let use_lia_cache = ref true
-let use_nia_cache = ref true
-let use_nra_cache = ref true
-let use_csdp_cache = ref true
-
-let () =
- let int_opt l vref =
- { optdepr = false
- ; optkey = l
- ; optread = (fun () -> Some !vref)
- ; optwrite =
- (fun x -> vref := match x with None -> max_depth | Some v -> v) }
- in
- let lia_enum_opt =
- { optdepr = false
- ; optkey = ["Lia"; "Enum"]
- ; optread = (fun () -> !lia_enum)
- ; optwrite = (fun x -> lia_enum := x) }
- in
- let solver_opt =
- { optdepr = false
- ; optkey = ["Simplex"]
- ; optread = (fun () -> !Certificate.use_simplex)
- ; optwrite = (fun x -> Certificate.use_simplex := x) }
- in
- let dump_file_opt =
- { optdepr = false
- ; optkey = ["Dump"; "Arith"]
- ; optread = (fun () -> !Certificate.dump_file)
- ; optwrite = (fun x -> Certificate.dump_file := x) }
- in
- let lia_cache_opt =
- { optdepr = false
- ; optkey = ["Lia"; "Cache"]
- ; optread = (fun () -> !use_lia_cache)
- ; optwrite = (fun x -> use_lia_cache := x) }
- in
- let nia_cache_opt =
- { optdepr = false
- ; optkey = ["Nia"; "Cache"]
- ; optread = (fun () -> !use_nia_cache)
- ; optwrite = (fun x -> use_nia_cache := x) }
- in
- let nra_cache_opt =
- { optdepr = false
- ; optkey = ["Nra"; "Cache"]
- ; optread = (fun () -> !use_nra_cache)
- ; optwrite = (fun x -> use_nra_cache := x) }
- in
- let () = declare_bool_option solver_opt in
- let () = declare_bool_option lia_cache_opt in
- let () = declare_bool_option nia_cache_opt in
- let () = declare_bool_option nra_cache_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 use_lia_cache =
+ declare_bool_option_and_ref ~depr:false ~key:["Lia"; "Cache"] ~value:true
+
+let use_nia_cache =
+ declare_bool_option_and_ref ~depr:false ~key:["Nia"; "Cache"] ~value:true
+
+let use_nra_cache =
+ declare_bool_option_and_ref ~depr:false ~key:["Nra"; "Cache"] ~value:true
+
+let use_csdp_cache () = true
(**
* Initialize a tag type to the Tag module declaration (see Mutils).
@@ -2101,7 +2058,7 @@ struct
let memo_opt use_cache cache_file f =
let memof = memo cache_file f in
- fun x -> if !use_cache then memof x else f x
+ fun x -> if use_cache () then memof x else f x
end
module CacheCsdp = MakeCache (struct
@@ -2281,7 +2238,7 @@ let memo_nra =
let linear_prover_Q =
{ name = "linear prover"
- ; get_option = get_lra_option
+ ; get_option = lra_proof_depth
; prover =
(fun (o, l) ->
lift_pexpr_prover (Certificate.linear_prover_with_cert o) l)
@@ -2292,7 +2249,7 @@ let linear_prover_Q =
let linear_prover_R =
{ name = "linear prover"
- ; get_option = get_lra_option
+ ; get_option = lra_proof_depth
; prover =
(fun (o, l) ->
lift_pexpr_prover (Certificate.linear_prover_with_cert o) l)
@@ -2303,7 +2260,7 @@ let linear_prover_R =
let nlinear_prover_R =
{ name = "nra"
- ; get_option = get_lra_option
+ ; get_option = lra_proof_depth
; prover = memo_nra
; hyps = hyps_of_cone
; compact = compact_cone
diff --git a/plugins/micromega/plugin_base.dune b/plugins/micromega/dune
index 4153d06161..33ad3a0138 100644
--- a/plugins/micromega/plugin_base.dune
+++ b/plugins/micromega/dune
@@ -20,3 +20,5 @@
(modules g_zify zify)
(synopsis "Coq's zify plugin")
(libraries coq.plugins.ltac))
+
+(coq.pp (modules g_micromega g_zify))
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index f157a807ad..9051bbb5ca 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -41,13 +41,21 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct
type mode = Closed | Open
type 'a t = {outch : out_channel; mutable status : mode; htbl : 'a Table.t}
- let finally f rst =
- try
- let res = f () in
- rst (); res
- with reraise ->
- (try rst () with any -> raise reraise);
- raise reraise
+ (* XXX: Move to Fun.protect once in Ocaml 4.08 *)
+ let fun_protect ~(finally : unit -> unit) work =
+ let finally_no_exn () =
+ let exception Finally_raised of exn in
+ try finally ()
+ with e ->
+ let bt = Printexc.get_raw_backtrace () in
+ Printexc.raise_with_backtrace (Finally_raised e) bt
+ in
+ match work () with
+ | result -> finally_no_exn (); result
+ | exception work_exn ->
+ let work_bt = Printexc.get_raw_backtrace () in
+ finally_no_exn ();
+ Printexc.raise_with_backtrace work_exn work_bt
let read_key_elem inch =
try Some (Marshal.from_channel inch) with
@@ -76,21 +84,23 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct
let unlock fd =
let pos = lseek fd 0 SEEK_CUR in
- try
- ignore (lseek fd 0 SEEK_SET);
- lockf fd F_ULOCK 1
- with Unix.Unix_error (_, _, _) ->
- ()
- (* Here, this is really bad news --
- there is a pending lock which could cause a deadlock.
- Should it be an anomaly or produce a warning ?
- *);
- ignore (lseek fd pos SEEK_SET)
+ let () =
+ try
+ ignore (lseek fd 0 SEEK_SET);
+ lockf fd F_ULOCK 1
+ with Unix.Unix_error (_, _, _) ->
+ (* Here, this is really bad news --
+ there is a pending lock which could cause a deadlock.
+ Should it be an anomaly or produce a warning ?
+ *)
+ ()
+ in
+ ignore (lseek fd pos SEEK_SET)
(* We make the assumption that an acquired lock can always be released *)
let do_under_lock kd fd f =
- if lock kd fd then finally f (fun () -> unlock fd) else f ()
+ if lock kd fd then fun_protect f ~finally:(fun () -> unlock fd) else f ()
let open_in f =
let flags = [O_RDONLY; O_CREAT] in
diff --git a/plugins/nsatz/plugin_base.dune b/plugins/nsatz/dune
index 9da5b39972..b921c9c408 100644
--- a/plugins/nsatz/plugin_base.dune
+++ b/plugins/nsatz/dune
@@ -3,3 +3,5 @@
(public_name coq.plugins.nsatz)
(synopsis "Coq's nsatz solver plugin")
(libraries num coq.plugins.ltac))
+
+(coq.pp (modules g_nsatz))
diff --git a/plugins/omega/plugin_base.dune b/plugins/omega/dune
index f512501c78..0db71ed6fb 100644
--- a/plugins/omega/plugin_base.dune
+++ b/plugins/omega/dune
@@ -3,3 +3,5 @@
(public_name coq.plugins.omega)
(synopsis "Coq's omega plugin")
(libraries coq.plugins.ltac))
+
+(coq.pp (modules g_omega))
diff --git a/plugins/rtauto/plugin_base.dune b/plugins/rtauto/dune
index 233845ae0f..43efa0eca5 100644
--- a/plugins/rtauto/plugin_base.dune
+++ b/plugins/rtauto/dune
@@ -3,3 +3,5 @@
(public_name coq.plugins.rtauto)
(synopsis "Coq's rtauto plugin")
(libraries coq.plugins.ltac))
+
+(coq.pp (modules g_rtauto))
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 537c37810e..1371c671a2 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -45,15 +45,11 @@ let reset_info () =
s_info.branch_successes <- 0;
s_info.nd_branching <- 0
-let pruning = ref true
-
-let opt_pruning=
- {optdepr=false;
- optkey=["Rtauto";"Pruning"];
- optread=(fun () -> !pruning);
- optwrite=(fun b -> pruning:=b)}
-
-let () = declare_bool_option opt_pruning
+let pruning =
+ declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Rtauto";"Pruning"]
+ ~value:true
type form=
Atom of int
@@ -182,7 +178,7 @@ let rec fill stack proof =
[] -> Complete proof.dep_it
| slice::super ->
if
- !pruning &&
+ pruning () &&
List.is_empty slice.proofs_done &&
not (slice.changes_goal && proof.dep_goal) &&
not (Int.Set.exists
@@ -529,7 +525,7 @@ let pp =
let pp_info () =
let count_info =
- if !pruning then
+ if pruning () then
str "Proof steps : " ++
int s_info.created_steps ++ str " created / " ++
int s_info.pruned_steps ++ str " pruned" ++ fnl () ++
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 63dae1417e..d464ec4c06 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -221,27 +221,17 @@ let build_env gamma=
mkApp(force node_count l_push,[|mkProp;p;e|]))
gamma.env (mkApp (force node_count l_empty,[|mkProp|]))
-open Goptions
-
-let verbose = ref false
-
-let opt_verbose=
- {optdepr=false;
- optkey=["Rtauto";"Verbose"];
- optread=(fun () -> !verbose);
- optwrite=(fun b -> verbose:=b)}
-
-let () = declare_bool_option opt_verbose
-
-let check = ref false
-
-let opt_check=
- {optdepr=false;
- optkey=["Rtauto";"Check"];
- optread=(fun () -> !check);
- optwrite=(fun b -> check:=b)}
-
-let () = declare_bool_option opt_check
+let verbose =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Rtauto";"Verbose"]
+ ~value:false
+
+let check =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Rtauto";"Check"]
+ ~value:false
open Pp
@@ -267,7 +257,7 @@ let rtauto_tac =
let () =
begin
reset_info ();
- if !verbose then
+ if verbose () then
Feedback.msg_info (str "Starting proof-search ...");
end in
let search_start_time = System.get_time () in
@@ -276,7 +266,7 @@ let rtauto_tac =
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);
@@ -292,7 +282,7 @@ let rtauto_tac =
let term=
applistc main (List.rev_map (fun (id,_) -> mkVar id.binder_name) 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 ++
@@ -306,14 +296,14 @@ let rtauto_tac =
let tac_start_time = System.get_time () in
let term = EConstr.of_constr term in
let result=
- if !check then
+ if check () then
Tactics.exact_check term
else
Tactics.exact_no_check term in
let tac_end_time = System.get_time () in
let () =
- if !check then Feedback.msg_info (str "Proof term type-checking is on");
- if !verbose then
+ if check () then Feedback.msg_info (str "Proof term type-checking is on");
+ if verbose () then
Feedback.msg_info (str "Internal tactic executed in " ++
System.fmt_time_difference tac_start_time tac_end_time) in
result
diff --git a/plugins/setoid_ring/plugin_base.dune b/plugins/setoid_ring/dune
index d83857edad..60522cd3f5 100644
--- a/plugins/setoid_ring/plugin_base.dune
+++ b/plugins/setoid_ring/dune
@@ -3,3 +3,5 @@
(public_name coq.plugins.setoid_ring)
(synopsis "Coq's setoid ring plugin")
(libraries coq.plugins.ltac))
+
+(coq.pp (modules g_newring))
diff --git a/plugins/ssr/plugin_base.dune b/plugins/ssr/dune
index a13524bb52..a117d09a16 100644
--- a/plugins/ssr/plugin_base.dune
+++ b/plugins/ssr/dune
@@ -5,3 +5,5 @@
(modules_without_implementation ssrast)
(flags :standard -open Gramlib)
(libraries coq.plugins.ssrmatching))
+
+(coq.pp (modules ssrvernac ssrparser))
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 01b12474dd..e0b083a70a 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -239,7 +239,7 @@ let interp_refine ist gl rc =
} in
let kind = Pretyping.OfType (pf_concl gl) in
let flags = {
- Pretyping.use_typeclasses = true;
+ Pretyping.use_typeclasses = Pretyping.UseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index df6189f212..4b78e64d98 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -402,7 +402,7 @@ let rec interp_search_about args accu = match args with
| [] -> accu
| (flag, arg) :: rem ->
fun gr env typ ->
- let ans = Search.search_about_filter arg gr env typ in
+ let ans = Search.search_filter arg gr env typ in
(if flag then ans else not ans) && interp_search_about rem accu gr env typ
let interp_search_arg arg =
diff --git a/plugins/ssrmatching/plugin_base.dune b/plugins/ssrmatching/dune
index 06f67c3774..629d723816 100644
--- a/plugins/ssrmatching/plugin_base.dune
+++ b/plugins/ssrmatching/dune
@@ -3,3 +3,5 @@
(public_name coq.plugins.ssrmatching)
(synopsis "Coq ssrmatching plugin")
(libraries coq.plugins.ltac))
+
+(coq.pp (modules g_ssrmatching))
diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/dune
index 512752135d..b395695c8a 100644
--- a/plugins/syntax/plugin_base.dune
+++ b/plugins/syntax/dune
@@ -32,3 +32,5 @@
(synopsis "Coq syntax plugin: float")
(modules float_syntax)
(libraries coq.vernac))
+
+(coq.pp (modules g_numeral g_string))
diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml
index dadce9a9ea..e0a9906689 100644
--- a/plugins/syntax/float_syntax.ml
+++ b/plugins/syntax/float_syntax.ml
@@ -22,8 +22,56 @@ let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
(*** Parsing for float in digital notation ***)
+let warn_inexact_float =
+ CWarnings.create ~name:"inexact-float" ~category:"parsing"
+ (fun (sn, f) ->
+ Pp.strbrk
+ (Printf.sprintf
+ "The constant %s is not a binary64 floating-point value. \
+ A closest value will be used and unambiguously printed %s."
+ sn (Float64.to_string f)))
+
let interp_float ?loc n =
- DAst.make ?loc (GFloat (Float64.of_string (NumTok.Signed.to_string n)))
+ let sn = NumTok.Signed.to_string n in
+ let f = Float64.of_string sn in
+ (* return true when f is not exactly equal to n,
+ this is only used to decide whether or not to display a warning
+ and does not play any actual role in the parsing *)
+ let inexact () = match Float64.classify f with
+ | Float64.(PInf | NInf | NaN) -> true
+ | Float64.(PZero | NZero) -> not (NumTok.Signed.is_zero n)
+ | Float64.(PNormal | NNormal | PSubn | NSubn) ->
+ let m, e =
+ let (_, i), f, e = NumTok.Signed.to_decimal_and_exponent n in
+ let i = NumTok.UnsignedNat.to_string i in
+ let f = match f with
+ | None -> "" | Some f -> NumTok.UnsignedNat.to_string f in
+ let e = match e with
+ | None -> "0" | Some e -> NumTok.SignedNat.to_string e in
+ Bigint.of_string (i ^ f),
+ (try int_of_string e with Failure _ -> 0) - String.length f in
+ let m', e' =
+ let m', e' = Float64.frshiftexp f in
+ let m' = Float64.normfr_mantissa m' in
+ let e' = Uint63.to_int_min e' 4096 - Float64.eshift - 53 in
+ Bigint.of_string (Uint63.to_string m'),
+ e' in
+ let c2, c5 = Bigint.(of_int 2, of_int 5) in
+ (* check m*5^e <> m'*2^e' *)
+ let check m e m' e' =
+ not (Bigint.(equal (mult m (pow c5 e)) (mult m' (pow c2 e')))) in
+ (* check m*5^e*2^e' <> m' *)
+ let check' m e e' m' =
+ not (Bigint.(equal (mult (mult m (pow c5 e)) (pow c2 e')) m')) in
+ (* we now have to check m*10^e <> m'*2^e' *)
+ if e >= 0 then
+ if e <= e' then check m e m' (e' - e)
+ else check' m e (e - e') m'
+ else (* e < 0 *)
+ if e' <= e then check m' (-e) m (e - e')
+ else check' m' (-e) (e' - e) m in
+ if inexact () then warn_inexact_float ?loc (sn, f);
+ DAst.make ?loc (GFloat f)
(* Pretty printing is already handled in constrextern.ml *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 20:01:57 +0000