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.ml14
-rw-r--r--plugins/funind/gen_principle.ml43
-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/rewrite.ml17
-rw-r--r--plugins/ltac/rewrite.mli4
13 files changed, 101 insertions, 82 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..2151ad7873 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -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..167cf37026 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -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/rewrite.ml b/plugins/ltac/rewrite.ml
index 4bc8d61258..f16d0717df 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 23:16:29 +0000