aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/derive/derive.ml11
-rw-r--r--plugins/derive/derive.mli2
-rw-r--r--plugins/extraction/extract_env.ml6
-rw-r--r--plugins/funind/functional_principles_proofs.ml16
-rw-r--r--plugins/funind/gen_principle.ml45
-rw-r--r--plugins/funind/gen_principle.mli2
-rw-r--r--plugins/funind/recdef.ml68
-rw-r--r--plugins/funind/recdef.mli2
-rw-r--r--plugins/ltac/extratactics.mlg4
-rw-r--r--plugins/ltac/g_ltac.mlg2
-rw-r--r--plugins/ltac/g_obligations.mlg8
-rw-r--r--plugins/ltac/leminv.ml2
-rw-r--r--plugins/ltac/rewrite.ml21
-rw-r--r--plugins/ltac/rewrite.mli4
-rw-r--r--plugins/ltac/tacentries.ml2
-rw-r--r--plugins/ltac/tacinterp.ml6
-rw-r--r--plugins/setoid_ring/newring.ml2
-rw-r--r--plugins/ssr/ssrcommon.ml4
-rw-r--r--plugins/ssr/ssrelim.ml2
19 files changed, 114 insertions, 95 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index e5665c59b8..027064b75f 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -15,7 +15,7 @@ open Context.Named.Declaration
(which can contain references to [f]) in the context extended by
[f:=?x]. When the proof ends, [f] is defined as the value of [?x]
and [lemma] as the proof. *)
-let start_deriving f suchthat name : Lemmas.t =
+let start_deriving f suchthat name : Declare.Proof.t =
let env = Global.env () in
let sigma = Evd.from_env env in
@@ -40,8 +40,7 @@ let start_deriving f suchthat name : Lemmas.t =
TNil sigma))))))
in
- let info = Lemmas.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in
- let lemma = Lemmas.start_dependent_lemma ~name ~poly ~info goals in
- Lemmas.pf_map (Declare.Proof.map_proof begin fun p ->
- Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
- end) lemma
+ let info = Declare.Info.make ~poly ~kind () in
+ let lemma = Declare.Proof.start_derive ~name ~f ~info goals in
+ Declare.Proof.map lemma ~f:(fun p ->
+ Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p)
diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli
index ef94c7e78f..06e7dacd36 100644
--- a/plugins/derive/derive.mli
+++ b/plugins/derive/derive.mli
@@ -16,4 +16,4 @@ val start_deriving
: Names.Id.t
-> Constrexpr.constr_expr
-> Names.Id.t
- -> Lemmas.t
+ -> Declare.Proof.t
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index a0627dbe63..af43c0517e 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -729,13 +729,13 @@ let extract_and_compile l =
(* Show the extraction of the current ongoing proof *)
let show_extraction ~pstate =
init ~inner:true false false;
- let prf = Declare.Proof.get_proof pstate in
- let sigma, env = Declare.get_current_context pstate in
+ let prf = Declare.Proof.get pstate in
+ let sigma, env = Declare.Proof.get_current_context pstate in
let trms = Proof.partial_proof prf in
let extr_term t =
let ast, ty = extract_constr env sigma t in
let mp = Lib.current_mp () in
- let l = Label.of_id (Declare.Proof.get_proof_name pstate) in
+ let l = Label.of_id (Declare.Proof.get_name pstate) in
let fake_ref = GlobRef.ConstRef (Constant.make2 mp l) in
let decl = Dterm (fake_ref, ast, ty) in
print_one_decl [] mp decl
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index b864b18887..9b578d4697 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -43,7 +43,7 @@ let finish_proof dynamic_infos g =
let refine c =
Proofview.V82.of_tactic
- (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c))
+ (Logic.refiner ~check:true EConstr.Unsafe.(to_constr c))
let thin l = Proofview.V82.of_tactic (Tactics.clear l)
let eq_constr sigma u v = EConstr.eq_constr_nounivs sigma u v
@@ -853,12 +853,16 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
(*i The next call to mk_equation_id is valid since we are
constructing the lemma Ensures by: obvious i*)
- let lemma =
- Lemmas.start_lemma ~name:(mk_equation_id f_id) ~poly:false evd lemma_type
+ let info = Declare.Info.make () in
+ let cinfo =
+ Declare.CInfo.make ~name:(mk_equation_id f_id) ~typ:lemma_type ()
+ in
+ let lemma = Declare.Proof.start ~cinfo ~info evd in
+ let lemma, _ =
+ Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma
in
- let lemma, _ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in
- let () =
- Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent ~idopt:None
+ let (_ : _ list) =
+ Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
in
evd
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 608155eb71..dcca694200 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -70,7 +70,7 @@ let build_newrecursive lnameargsardef =
CErrors.user_err ~hdr:"Function"
(Pp.str "Body of Function must be given")
in
- States.with_state_protection (List.map f) lnameargsardef
+ Vernacstate.System.protect (List.map f) lnameargsardef
in
(recdef, rec_impls)
@@ -319,7 +319,7 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts
let entry = Declare.definition_entry ~univs ?types body in
let (_ : Names.GlobRef.t) =
Declare.declare_entry ~name:new_princ_name ~hook
- ~scope:(Declare.Global Declare.ImportDefaultBehavior)
+ ~scope:(Locality.Global Locality.ImportDefaultBehavior)
~kind:Decls.(IsProof Theorem)
~impargs:[] ~uctx entry
in
@@ -400,7 +400,7 @@ let register_struct is_rec fixpoint_exprl =
Pp.(str "Body of Function must be given")
in
ComDefinition.do_definition ~name:fname.CAst.v ~poly:false
- ~scope:(Declare.Global Declare.ImportDefaultBehavior)
+ ~scope:(Locality.Global Locality.ImportDefaultBehavior)
~kind:Decls.Definition univs binders None body (Some rtype);
let evd, rev_pconstants =
List.fold_left
@@ -419,7 +419,7 @@ let register_struct is_rec fixpoint_exprl =
(None, evd, List.rev rev_pconstants)
| _ ->
ComFixpoint.do_fixpoint
- ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~poly:false
+ ~scope:(Locality.Global Locality.ImportDefaultBehavior) ~poly:false
fixpoint_exprl;
let evd, rev_pconstants =
List.fold_left
@@ -1370,12 +1370,12 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : _ list =
| None -> raise Not_found
| Some finfos -> finfos
in
- let open Declare in
match finfos.equation_lemma with
- | None -> Transparent (* non recursive definition *)
+ | None -> Vernacexpr.Transparent (* non recursive definition *)
| Some equation ->
- if Declareops.is_opaque (Global.lookup_constant equation) then Opaque
- else Transparent
+ if Declareops.is_opaque (Global.lookup_constant equation) then
+ Vernacexpr.Opaque
+ else Vernacexpr.Transparent
in
let body, typ, univs, _hook, sigma0 =
try
@@ -1518,12 +1518,14 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
i*)
let lem_id = mk_correct_id f_id in
let typ, _ = lemmas_types_infos.(i) in
- let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false !evd typ in
+ let info = Declare.Info.make () in
+ let cinfo = Declare.CInfo.make ~name:lem_id ~typ () in
+ let lemma = Declare.Proof.start ~cinfo ~info !evd in
let lemma =
- fst @@ Lemmas.by (Proofview.V82.tactic (proving_tac i)) lemma
+ fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma
in
- let () =
- Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent
+ let (_ : GlobRef.t list) =
+ Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
~idopt:None
in
let finfo =
@@ -1580,21 +1582,22 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
Ensures by: obvious
i*)
let lem_id = mk_complete_id f_id in
- let lemma =
- Lemmas.start_lemma ~name:lem_id ~poly:false sigma
- (fst lemmas_types_infos.(i))
+ let info = Declare.Info.make () in
+ let cinfo =
+ Declare.CInfo.make ~name:lem_id ~typ:(fst lemmas_types_infos.(i)) ()
in
+ let lemma = Declare.Proof.start ~cinfo sigma ~info in
let lemma =
fst
- (Lemmas.by
+ (Declare.Proof.by
(Proofview.V82.tactic
(observe_tac
("prove completeness (" ^ Id.to_string f_id ^ ")")
(proving_tac i)))
lemma)
in
- let () =
- Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent
+ let (_ : _ list) =
+ Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
~idopt:None
in
let finfo =
@@ -1769,7 +1772,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt
using_lemmas args ret_type body
let do_generate_principle_aux pconstants on_error register_built
- interactive_proof fixpoint_exprl : Lemmas.t option =
+ interactive_proof fixpoint_exprl : Declare.Proof.t option =
List.iter
(fun {Vernacexpr.notations} ->
if not (List.is_empty notations) then
@@ -2155,7 +2158,7 @@ let make_graph (f_ref : GlobRef.t) =
(* *************** statically typed entrypoints ************************* *)
-let do_generate_principle_interactive fixl : Lemmas.t =
+let do_generate_principle_interactive fixl : Declare.Proof.t =
match do_generate_principle_aux [] warning_error true true fixl with
| Some lemma -> lemma
| None ->
@@ -2199,7 +2202,7 @@ let build_scheme fas =
List.iter2
(fun (princ_id, _, _) (body, types, univs, opaque) ->
let (_ : Constant.t) =
- let opaque = if opaque = Declare.Opaque then true else false in
+ let opaque = if opaque = Vernacexpr.Opaque then true else false in
let def_entry = Declare.definition_entry ~univs ~opaque ?types body in
Declare.declare_constant ~name:princ_id
~kind:Decls.(IsProof Theorem)
diff --git a/plugins/funind/gen_principle.mli b/plugins/funind/gen_principle.mli
index 3c04d6cb7d..28751c4501 100644
--- a/plugins/funind/gen_principle.mli
+++ b/plugins/funind/gen_principle.mli
@@ -12,7 +12,7 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit
val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit
val do_generate_principle_interactive :
- Vernacexpr.fixpoint_expr list -> Lemmas.t
+ Vernacexpr.fixpoint_expr list -> Declare.Proof.t
val do_generate_principle : Vernacexpr.fixpoint_expr list -> unit
val make_graph : Names.GlobRef.t -> unit
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9b2d9c4815..884792cc15 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -58,7 +58,10 @@ let declare_fun name kind ?univs value =
(Declare.declare_constant ~name ~kind (Declare.DefinitionEntry ce))
let defined lemma =
- Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent ~idopt:None
+ let (_ : _ list) =
+ Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
+ in
+ ()
let def_of_const t =
match Constr.kind t with
@@ -1343,7 +1346,7 @@ let whole_start concl_tac nb_args is_mes func input_type relation rec_arg_num :
g
let get_current_subgoals_types pstate =
- let p = Declare.Proof.get_proof pstate in
+ let p = Declare.Proof.get pstate in
let Proof.{goals = sgs; sigma; _} = Proof.data p in
(sigma, List.map (Goal.V82.abstract_type sigma) sgs)
@@ -1405,7 +1408,7 @@ let clear_goals sigma =
List.map clear_goal
let build_new_goal_type lemma =
- let sigma, sub_gls_types = Lemmas.pf_fold get_current_subgoals_types lemma in
+ let sigma, sub_gls_types = get_current_subgoals_types lemma in
(* Pp.msgnl (str "sub_gls_types1 := " ++ Util.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *)
let sub_gls_types = clear_goals sigma sub_gls_types in
(* Pp.msgnl (str "sub_gls_types2 := " ++ Pp.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *)
@@ -1414,16 +1417,17 @@ let build_new_goal_type lemma =
let is_opaque_constant c =
let cb = Global.lookup_constant c in
+ let open Vernacexpr in
match cb.Declarations.const_body with
- | Declarations.OpaqueDef _ -> Declare.Opaque
- | Declarations.Undef _ -> Declare.Opaque
- | Declarations.Def _ -> Declare.Transparent
- | Declarations.Primitive _ -> Declare.Opaque
+ | Declarations.OpaqueDef _ -> Opaque
+ | Declarations.Undef _ -> Opaque
+ | Declarations.Def _ -> Transparent
+ | Declarations.Primitive _ -> Opaque
let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
(gls_type, decompose_and_tac, nb_goal) =
(* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
- let current_proof_name = Lemmas.pf_fold Declare.Proof.get_proof_name lemma in
+ let current_proof_name = Declare.Proof.get_name lemma in
let name =
match goal_name with
| Some s -> s
@@ -1488,18 +1492,20 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
[Hints.Hint_db.empty TransparentState.empty false] ]))
in
let lemma = build_proof env (Evd.from_env env) start_tac end_tac in
- Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None
- in
- let info = Lemmas.Info.make ~hook:(Declare.Hook.make hook) () in
- let lemma =
- Lemmas.start_lemma ~name:na ~poly:false (* FIXME *) ~info sigma gls_type
+ let (_ : _ list) =
+ Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None
+ in
+ ()
in
+ let info = Declare.Info.make ~hook:(Declare.Hook.make hook) () in
+ let cinfo = Declare.CInfo.make ~name:na ~typ:gls_type () in
+ let lemma = Declare.Proof.start ~cinfo ~info sigma in
let lemma =
if Indfun_common.is_strict_tcc () then
- fst @@ Lemmas.by (Proofview.V82.tactic tclIDTAC) lemma
+ fst @@ Declare.Proof.by (Proofview.V82.tactic tclIDTAC) lemma
else
fst
- @@ Lemmas.by
+ @@ Declare.Proof.by
(Proofview.V82.tactic (fun g ->
tclTHEN decompose_and_tac
(tclORELSE
@@ -1521,27 +1527,28 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
g))
lemma
in
- if Lemmas.(pf_fold Declare.Proof.get_open_goals) lemma = 0 then (
- defined lemma; None )
+ if Declare.Proof.get_open_goals lemma = 0 then (defined lemma; None)
else Some lemma
let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes
fonctional_ref input_type relation rec_arg_num thm_name using_lemmas nb_args
ctx hook =
let start_proof env ctx tac_start tac_end =
- let info = Lemmas.Info.make ~hook () in
- let lemma =
- Lemmas.start_lemma ~name:thm_name ~poly:false (*FIXME*) ~info ctx
- (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref))
+ let cinfo =
+ Declare.CInfo.make ~name:thm_name
+ ~typ:(EConstr.of_constr (compute_terminate_type nb_args fonctional_ref))
+ ()
in
+ let info = Declare.Info.make ~hook () in
+ let lemma = Declare.Proof.start ~cinfo ~info ctx in
let lemma =
fst
- @@ Lemmas.by
+ @@ Declare.Proof.by
(New.observe_tac (fun _ _ -> str "starting_tac") tac_start)
lemma
in
fst
- @@ Lemmas.by
+ @@ Declare.Proof.by
(Proofview.V82.tactic
(observe_tac
(fun _ _ -> str "whole_start")
@@ -1602,13 +1609,16 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
let evd = Evd.from_ctx uctx in
let f_constr = constr_of_monomorphic_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
- let lemma =
- Lemmas.start_lemma ~name:eq_name ~poly:false evd
- (EConstr.of_constr equation_lemma_type)
+ let info = Declare.Info.make () in
+ let cinfo =
+ Declare.CInfo.make ~name:eq_name
+ ~typ:(EConstr.of_constr equation_lemma_type)
+ ()
in
+ let lemma = Declare.Proof.start ~cinfo evd ~info in
let lemma =
fst
- @@ Lemmas.by
+ @@ Declare.Proof.by
(Proofview.V82.tactic
(start_equation f_ref terminate_ref (fun x ->
prove_eq
@@ -1642,7 +1652,7 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
in
let _ =
Flags.silently
- (fun () -> Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None)
+ (fun () -> Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None)
()
in
()
@@ -1651,7 +1661,7 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
let recursive_definition ~interactive_proof ~is_mes function_name rec_impls
type_of_f r rec_arg_num eq generate_induction_principle using_lemmas :
- Lemmas.t option =
+ Declare.Proof.t option =
let open Term in
let open Constr in
let open CVars in
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 4e5146e37c..2612f2b63e 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -25,4 +25,4 @@ val recursive_definition :
-> EConstr.constr
-> unit)
-> Constrexpr.constr_expr list
- -> Lemmas.t option
+ -> Declare.Proof.t option
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index ffb597d4cb..40c64a1c26 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -918,7 +918,7 @@ END
VERNAC COMMAND EXTEND GrabEvars STATE proof
| [ "Grab" "Existential" "Variables" ]
=> { classify_as_proofstep }
- -> { fun ~pstate -> Declare.Proof.map_proof (fun p -> Proof.V82.grab_evars p) pstate }
+ -> { fun ~pstate -> Declare.Proof.map ~f:(fun p -> Proof.V82.grab_evars p) pstate }
END
(* Shelves all the goals under focus. *)
@@ -950,7 +950,7 @@ END
VERNAC COMMAND EXTEND Unshelve STATE proof
| [ "Unshelve" ]
=> { classify_as_proofstep }
- -> { fun ~pstate -> Declare.Proof.map_proof (fun p -> Proof.unshelve p) pstate }
+ -> { fun ~pstate -> Declare.Proof.map ~f:(fun p -> Proof.unshelve p) pstate }
END
(* Gives up on the goals under focus: the goals are considered solved,
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 996f6b3eb3..114acaa412 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -363,7 +363,7 @@ let print_info_trace =
let vernac_solve ~pstate n info tcom b =
let open Goal_select in
- let pstate, status = Declare.Proof.map_fold_proof_endline (fun etac p ->
+ let pstate, status = Declare.Proof.map_fold_endline ~f:(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
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 498b33d1a8..81ee6ed5bb 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -28,7 +28,7 @@ let () =
let tac = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
snd (get_default_tactic ())
end in
- Obligations.default_tactic := tac
+ Declare.Obls.default_tactic := tac
let with_tac f tac =
let env = Genintern.empty_glob_sign (Global.env ()) in
@@ -78,10 +78,10 @@ GRAMMAR EXTEND Gram
{
-open Obligations
+open Declare.Obls
-let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac
-let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac
+let obligation obl tac = with_tac (fun t -> obligation obl t) tac
+let next_obligation obl tac = with_tac (fun t -> next_obligation obl t) tac
let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml
index 5a8ec404ee..0024d1a4ba 100644
--- a/plugins/ltac/leminv.ml
+++ b/plugins/ltac/leminv.ml
@@ -261,7 +261,7 @@ let lemInv id c =
try
let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_get_type_of gls c) in
let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in
- Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false
+ Clenv.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false
with
| NoSuchBinding ->
user_err
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 4bc8d61258..40dea90c00 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1567,7 +1567,7 @@ let assert_replacing id newt tac =
let newfail n s =
let info = Exninfo.reify () in
- Proofview.tclZERO ~info (Refiner.FailError (n, lazy s))
+ Proofview.tclZERO ~info (Tacticals.FailError (n, lazy s))
let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let open Proofview.Notations in
@@ -1656,7 +1656,7 @@ let cl_rewrite_clause_strat progress strat clause =
(fun (e, info) -> match e with
| RewriteFailure e ->
tclZEROMSG ~info (str"setoid rewrite failed: " ++ e)
- | Refiner.FailError (n, pp) ->
+ | Tacticals.FailError (n, pp) ->
tclFAIL ~info n (str"setoid rewrite failed: " ++ Lazy.force pp)
| e ->
Proofview.tclZERO ~info e))
@@ -1900,10 +1900,12 @@ let declare_projection name instance_id r =
in it_mkProd_or_LetIn ccl ctx
in
let types = Some (it_mkProd_or_LetIn typ ctx) in
- let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in
+ let kind, opaque, scope = Decls.(IsDefinition Definition), false, Locality.Global Locality.ImportDefaultBehavior in
let impargs, udecl = [], UState.default_univ_decl in
+ let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in
+ let info = Declare.Info.make ~scope ~kind ~udecl ~poly () in
let _r : GlobRef.t =
- Declare.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
+ Declare.declare_definition ~cinfo ~info ~opaque ~body sigma
in ()
let build_morphism_signature env sigma m =
@@ -1967,7 +1969,7 @@ let add_morphism_as_parameter atts m n : unit =
let env = Global.env () in
let evd = Evd.from_env env in
let poly = atts.polymorphic in
- let kind, opaque, scope = Decls.(IsAssumption Logical), false, Declare.Global Declare.ImportDefaultBehavior in
+ let kind, opaque, scope = Decls.(IsAssumption Logical), false, Locality.Global Locality.ImportDefaultBehavior in
let impargs, udecl = [], UState.default_univ_decl in
let evd, types = build_morphism_signature env evd m in
let evd, pe = Declare.prepare_parameter ~poly ~udecl ~types evd in
@@ -1978,7 +1980,7 @@ let add_morphism_as_parameter atts m n : unit =
(PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global cst);
declare_projection n instance_id cst
-let add_morphism_interactive atts m n : Lemmas.t =
+let add_morphism_interactive atts m n : Declare.Proof.t =
init_setoid ();
let instance_id = add_suffix n "_Proper" in
let env = Global.env () in
@@ -1996,11 +1998,12 @@ let add_morphism_interactive atts m n : Lemmas.t =
| _ -> assert false
in
let hook = Declare.Hook.make hook in
- let info = Lemmas.Info.make ~hook ~kind () in
Flags.silently
(fun () ->
- let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info evd morph in
- fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
+ let cinfo = Declare.CInfo.make ~name:instance_id ~typ:morph () in
+ let info = Declare.Info.make ~poly ~hook ~kind () in
+ let lemma = Declare.Proof.start ~cinfo ~info evd in
+ fst (Declare.Proof.by (Tacinterp.interp tac) lemma)) ()
let add_morphism atts binders m s n =
init_setoid ();
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 1161c84e6a..60a66dd861 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -101,7 +101,7 @@ val add_setoid
-> Id.t
-> unit
-val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Lemmas.t
+val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Declare.Proof.t
val add_morphism_as_parameter : rewrite_attributes -> constr_expr -> Id.t -> unit
val add_morphism
@@ -110,7 +110,7 @@ val add_morphism
-> constr_expr
-> constr_expr
-> Id.t
- -> Lemmas.t
+ -> Declare.Proof.t
val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index e6c59f446d..f8c25d5dd0 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -489,7 +489,7 @@ let register_ltac local ?deprecation tacl =
in
(* STATE XXX: Review what is going on here. Why does this needs
protection? Why is not the STM level protection enough? Fishy *)
- let defs = States.with_state_protection defs () in
+ let defs = Vernacstate.System.protect defs () in
let iter (def, tac) = match def with
| NewTac id ->
Tacenv.register_ltac false local id tac ?deprecation;
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 705a1a62ce..fdebe14a23 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -22,7 +22,6 @@ open Util
open Names
open Nameops
open Libnames
-open Refiner
open Tacmach.New
open Tactic_debug
open Constrexpr
@@ -1103,8 +1102,8 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
| TacProgress tac -> Tacticals.New.tclPROGRESS (interp_tactic ist tac)
| TacShowHyps tac ->
Proofview.V82.tactic begin
- tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
- end [@ocaml.warning "-3"]
+ Tacticals.tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
+ end
| TacAbstract (t,ido) ->
let call = LtacMLCall tac in
let trace = push_trace(None,call) ist in
@@ -1442,6 +1441,7 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
if the left-hand side fails. *)
and interp_match_successes lz ist s =
let general =
+ let open Tacticals in
let break (e, info) = match e with
| FailError (0, _) -> None
| FailError (n, s) -> Some (FailError (pred n, s), info)
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index e7c75e029e..878f7a834e 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -201,7 +201,7 @@ let exec_tactic env evd n f args =
(* Evaluate the whole result *)
let gl = dummy_goal env evd in
let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in
- let evd = Evd.minimize_universes (Refiner.project gls) in
+ let evd = Evd.minimize_universes gls.Evd.sigma in
let nf c = constr_of evd c in
Array.map nf !tactic_res, Evd.universe_context_set evd
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 01e8daf82d..5f463f8de4 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -748,7 +748,7 @@ let pf_abs_cterm gl n c0 = abs_cterm (pf_env gl) (project gl) n c0
(* }}} *)
let pf_merge_uc uc gl =
- re_sig (sig_it gl) (Evd.merge_universe_context (Refiner.project gl) uc)
+ re_sig (sig_it gl) (Evd.merge_universe_context gl.Evd.sigma uc)
let pf_merge_uc_of sigma gl =
let ucst = Evd.evar_universe_context sigma in
pf_merge_uc ucst gl
@@ -1029,7 +1029,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t =
pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t));
Proofview.(V82.of_tactic
(Tacticals.New.tclTHENLIST [
- Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t);
+ Logic.refiner ~check:false EConstr.Unsafe.(to_constr t);
(if first_goes_last then cycle 1 else tclUNIT ())
])) gl
end
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 8e75ba7a2b..a12b4aad11 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -482,7 +482,7 @@ let revtoptac n0 =
let dc, cl = EConstr.decompose_prod_n_assum sigma n concl in
let dc' = dc @ [Context.Rel.Declaration.LocalAssum(make_annot (Name rev_id) Sorts.Relevant, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in
let f = EConstr.it_mkLambda_or_LetIn (mkEtaApp (EConstr.mkRel (n + 1)) (-n) 1) dc' in
- Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|])))
+ Logic.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|])))
end
let equality_inj l b id c =
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 14:51:40 +0000