aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/derive/derive.ml24
-rw-r--r--plugins/derive/derive.mli6
-rw-r--r--plugins/derive/g_derive.mlg2
-rw-r--r--plugins/extraction/extract_env.ml4
-rw-r--r--plugins/funind/functional_principles_proofs.ml16
-rw-r--r--plugins/funind/functional_principles_types.ml8
-rw-r--r--plugins/funind/indfun.ml24
-rw-r--r--plugins/funind/indfun.mli2
-rw-r--r--plugins/funind/invfun.ml16
-rw-r--r--plugins/funind/recdef.ml87
-rw-r--r--plugins/funind/recdef.mli34
-rw-r--r--plugins/ltac/rewrite.ml11
-rw-r--r--plugins/ltac/rewrite.mli6
13 files changed, 115 insertions, 125 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 7c0f269481..fd5b3a7e48 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -22,7 +22,7 @@ let map_const_entry_body (f:constr->constr) (x:Safe_typing.private_constants Ent
(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 lemma =
+let start_deriving f suchthat name : Lemmas.t =
let env = Global.env () in
let sigma = Evd.from_env env in
@@ -48,7 +48,6 @@ let start_deriving f suchthat lemma =
(* The terminator handles the registering of constants when the proof is closed. *)
let terminator com =
- let open Proof_global in
(* Extracts the relevant information from the proof. [Admitted]
and [Save] result in user errors. [opaque] is [true] if the
proof was concluded by [Qed], and [false] if [Defined]. [f_def]
@@ -56,10 +55,10 @@ let start_deriving f suchthat lemma =
[suchthat], respectively. *)
let (opaque,f_def,lemma_def) =
match com with
- | Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.")
- | Proved (_,Some _,_) ->
+ | Lemmas.Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.")
+ | Lemmas.Proved (_,Some _,_) ->
CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.")
- | Proved (opaque, None, obj) ->
+ | Lemmas.Proved (opaque, None, obj) ->
match Proof_global.(obj.entries) with
| [_;f_def;lemma_def] ->
opaque <> Proof_global.Transparent , f_def , lemma_def
@@ -97,12 +96,11 @@ let start_deriving f suchthat lemma =
Entries.DefinitionEntry lemma_def ,
Decl_kinds.(IsProof Proposition)
in
- ignore (Declare.declare_constant lemma lemma_def)
- in
+ ignore (Declare.declare_constant name lemma_def)
+ in
- let terminator = Proof_global.make_terminator terminator in
- let pstate = Proof_global.start_dependent_proof lemma kind goals terminator in
- Proof_global.modify_proof begin fun p ->
- let p,_,() = Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p in
- p
- end pstate
+ let terminator ?hook _ = Lemmas.make_terminator terminator in
+ let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in
+ Lemmas.simple_with_proof begin fun _ p ->
+ Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
+ end lemma
diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli
index 6bb923118e..ffbc726e22 100644
--- a/plugins/derive/derive.mli
+++ b/plugins/derive/derive.mli
@@ -12,4 +12,8 @@
(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. *)
-val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.t
+val start_deriving
+ : Names.Id.t
+ -> Constrexpr.constr_expr
+ -> Names.Id.t
+ -> Lemmas.t
diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg
index 526989fdf3..6c9cd66f96 100644
--- a/plugins/derive/g_derive.mlg
+++ b/plugins/derive/g_derive.mlg
@@ -24,5 +24,5 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac
VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } STATE open_proof
| [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] ->
- { Derive.(start_deriving f suchthat lemma) }
+ { Derive.start_deriving f suchthat lemma }
END
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index c5439ffaf6..4cd34100bc 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -752,13 +752,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 = Proof_global.give_me_the_proof pstate in
+ let prf = Proof_global.get_proof pstate in
let sigma, env = Pfedit.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 (Proof_global.get_current_proof_name pstate) in
+ let l = Label.of_id (Proof_global.get_proof_name pstate) in
let fake_ref = 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 b3a799fb6a..b8e1286b9e 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -990,7 +990,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
]
in
(* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *)
- let pstate = Lemmas.start_proof
+ let lemma = Lemmas.start_lemma
(*i The next call to mk_equation_id is valid since we are constructing the lemma
Ensures by: obvious
i*)
@@ -999,12 +999,10 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
evd
lemma_type
in
- let pstate,_ = Pfedit.by (Proofview.V82.tactic prove_replacement) pstate in
- let ontop = Proof_global.push ~ontop:None pstate in
- ignore(Lemmas.save_proof_proved ?proof:None ~ontop ~opaque:Proof_global.Transparent ~idopt:None);
+ let lemma,_ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in
+ let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
evd
-
let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g =
let equation_lemma =
try
@@ -1725,11 +1723,3 @@ let prove_principle_for_gen
]
gl
-
-
-
-
-
-
-
-
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 965ce68811..d1e540cceb 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -308,8 +308,8 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in
evd := sigma;
let hook = Lemmas.mk_hook (hook new_principle_type) in
- let pstate =
- Lemmas.start_proof
+ let lemma =
+ Lemmas.start_lemma
new_princ_name
Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
!evd
@@ -317,7 +317,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
in
(* let _tim1 = System.get_time () in *)
let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in
- let pstate,_ = Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)) pstate in
+ let lemma,_ = Lemmas.by (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)) lemma in
(* let _tim2 = System.get_time () in *)
(* begin *)
(* let dur1 = System.time_difference tim1 tim2 in *)
@@ -325,7 +325,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
(* end; *)
let open Proof_global in
- let { id; entries; persistence } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pstate in
+ let { id; entries; persistence } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in
match entries with
| [entry] ->
(id,(entry,persistence)), hook
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 7070f01c6f..d710f4490d 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -634,9 +634,9 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex
let do_generate_principle_aux pconstants on_error register_built interactive_proof
- (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.t option =
+ (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Lemmas.t option =
List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl;
- let pstate, _is_struct =
+ let lemma, _is_struct =
match fixpoint_exprl with
| [((_,Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)},_,_,_),_) as fixpoint_expr] ->
let (((({CAst.v=name},pl),_,args,types,body)),_) as fixpoint_expr =
@@ -702,7 +702,7 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
(* ok all the expressions are structural *)
let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
let is_rec = List.exists (is_rec fix_names) recdefs in
- let pstate,evd,pconstants =
+ let lemma,evd,pconstants =
if register_built
then register_struct is_rec fixpoint_exprl
else None, Evd.from_env (Global.env ()), pconstants
@@ -720,9 +720,9 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
(Functional_principles_proofs.prove_princ_for_struct evd interactive_proof);
if register_built then
begin derive_inversion fix_names; end;
- pstate, true
+ lemma, true
in
- pstate
+ lemma
let rec add_args id new_args = CAst.map (function
| CRef (qid,_) as b ->
@@ -911,18 +911,18 @@ let make_graph (f_ref : GlobRef.t) =
(* *************** statically typed entrypoints ************************* *)
-let do_generate_principle_interactive fixl : Proof_global.t =
+let do_generate_principle_interactive fixl : Lemmas.t =
match
do_generate_principle_aux [] warning_error true true fixl
with
- | Some pstate -> pstate
+ | Some lemma -> lemma
| None ->
- CErrors.anomaly
- (Pp.str"indfun: leaving no open proof in interactive mode")
+ CErrors.anomaly
+ (Pp.str"indfun: leaving no open proof in interactive mode")
let do_generate_principle fixl : unit =
match do_generate_principle_aux [] warning_error true false fixl with
- | Some _pstate ->
- CErrors.anomaly
- (Pp.str"indfun: leaving a goal open in non-interactive mode")
+ | Some _lemma ->
+ CErrors.anomaly
+ (Pp.str"indfun: leaving a goal open in non-interactive mode")
| None -> ()
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 1ba245a45d..3bc52272ac 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -10,7 +10,7 @@ val do_generate_principle :
val do_generate_principle_interactive :
(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list ->
- Proof_global.t
+ Lemmas.t
val functional_induction :
bool ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 8a16326ba3..857b7df96f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -803,15 +803,15 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
i*)
let lem_id = mk_correct_id f_id in
let (typ,_) = lemmas_types_infos.(i) in
- let pstate = Lemmas.start_proof
+ let lemma = Lemmas.start_lemma
lem_id
Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
!evd
typ in
- let pstate = fst @@ Pfedit.by
+ let lemma = fst @@ Lemmas.by
(Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
- (proving_tac i))) pstate in
- let () = Lemmas.save_pstate_proved ~pstate ~opaque:Proof_global.Transparent ~idopt:None in
+ (proving_tac i))) lemma in
+ let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
let finfo = find_Function_infos (fst f_as_constant) in
(* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
let _,lem_cst_constr = Evd.fresh_global
@@ -865,13 +865,13 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
Ensures by: obvious
i*)
let lem_id = mk_complete_id f_id in
- let pstate = Lemmas.start_proof lem_id
+ let lemma = Lemmas.start_lemma lem_id
Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma
(fst lemmas_types_infos.(i)) in
- let pstate = fst (Pfedit.by
+ let lemma = fst (Lemmas.by
(Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
- (proving_tac i))) pstate) in
- let () = Lemmas.save_pstate_proved ~pstate ~opaque:Proof_global.Transparent ~idopt:None in
+ (proving_tac i))) lemma) in
+ let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
let finfo = find_Function_infos (fst f_as_constant) in
let _,lem_cst_constr = Evd.fresh_global
(Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5bedb360d1..17d962f30f 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -34,7 +34,6 @@ open Declare
open Decl_kinds
open Tacred
open Goal
-open Pfedit
open Glob_term
open Pretyping
open Termops
@@ -72,7 +71,8 @@ let declare_fun f_id kind ?univs value =
let ce = definition_entry ?univs value (*FIXME *) in
ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
-let defined pstate = Lemmas.save_pstate_proved ~pstate ~opaque:Proof_global.Transparent ~idopt:None
+let defined lemma =
+ Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None
let def_of_const t =
match (Constr.kind t) with
@@ -1221,7 +1221,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
end
let get_current_subgoals_types pstate =
- let p = Proof_global.give_me_the_proof pstate in
+ let p = Proof_global.get_proof pstate in
let Proof.{ goals=sgs; sigma; _ } = Proof.data p in
sigma, List.map (Goal.V82.abstract_type sigma) sgs
@@ -1281,8 +1281,8 @@ let clear_goals sigma =
List.map clear_goal
-let build_new_goal_type pstate =
- let sigma, sub_gls_types = get_current_subgoals_types pstate in
+let build_new_goal_type lemma =
+ let sigma, sub_gls_types = Lemmas.pf_fold 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); *)
@@ -1297,9 +1297,9 @@ let is_opaque_constant c =
| Declarations.Def _ -> Proof_global.Transparent
| Declarations.Primitive _ -> Proof_global.Opaque
-let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) =
+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 = Proof_global.get_current_proof_name pstate in
+ let current_proof_name = Lemmas.pf_fold Proof_global.get_proof_name lemma in
let name = match goal_name with
| Some s -> s
| None ->
@@ -1323,7 +1323,7 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type
let lid = ref [] in
let h_num = ref (-1) in
let env = Global.env () in
- let pstate = build_proof env (Evd.from_env env)
+ let lemma = build_proof env (Evd.from_env env)
( fun gls ->
let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
observe_tclTHENLIST (fun _ _ -> str "")
@@ -1367,17 +1367,17 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type
)
g)
in
- Lemmas.save_pstate_proved ~pstate ~opaque:opacity ~idopt:None
+ Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None
in
- let pstate = Lemmas.start_proof
+ let lemma = Lemmas.start_lemma
na
Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma)
sigma gls_type ~hook:(Lemmas.mk_hook hook) in
- let pstate = if Indfun_common.is_strict_tcc ()
+ let lemma = if Indfun_common.is_strict_tcc ()
then
- fst @@ by (Proofview.V82.tactic (tclIDTAC)) pstate
+ fst @@ Lemmas.by (Proofview.V82.tactic (tclIDTAC)) lemma
else
- fst @@ by (Proofview.V82.tactic begin
+ fst @@ Lemmas.by (Proofview.V82.tactic begin
fun g ->
tclTHEN
(decompose_and_tac)
@@ -1393,9 +1393,9 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type
)
using_lemmas)
) tclIDTAC)
- g end) pstate
+ g end) lemma
in
- if Proof_global.get_open_goals pstate = 0 then (defined pstate; None) else Some pstate
+ if Lemmas.(pf_fold Proof_global.get_open_goals) lemma = 0 then (defined lemma; None) else Some lemma
let com_terminate
interactive_proof
@@ -1410,26 +1410,26 @@ let com_terminate
nb_args ctx
hook =
let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
- let pstate = Lemmas.start_proof thm_name
+ let lemma = Lemmas.start_lemma thm_name
(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook in
- let pstate = fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "starting_tac") tac_start)) pstate in
- fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
- input_type relation rec_arg_num ))) pstate
+ let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "starting_tac") tac_start)) lemma in
+ fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
+ input_type relation rec_arg_num ))) lemma
in
- let pstate = start_proof Global.(env ()) ctx tclIDTAC tclIDTAC in
+ let lemma = start_proof Global.(env ()) ctx tclIDTAC tclIDTAC in
try
- let sigma, new_goal_type = build_new_goal_type pstate in
+ let sigma, new_goal_type = build_new_goal_type lemma in
let sigma = Evd.from_ctx (Evd.evar_universe_context sigma) in
- open_new_goal pstate start_proof sigma
+ open_new_goal ~lemma start_proof sigma
using_lemmas tcc_lemma_ref
(Some tcc_lemma_name)
(new_goal_type)
with EmptySubgoals ->
(* a non recursive function declared with measure ! *)
tcc_lemma_ref := Not_needed;
- if interactive_proof then Some pstate
- else (defined pstate; None)
+ if interactive_proof then Some lemma
+ else (defined lemma; None)
let start_equation (f:GlobRef.t) (term_f:GlobRef.t)
(cont_tactic:Id.t list -> tactic) g =
@@ -1457,9 +1457,9 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
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 pstate = Lemmas.start_proof eq_name (Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd
+ let lemma = Lemmas.start_lemma eq_name (Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd
(EConstr.of_constr equation_lemma_type) in
- let pstate = fst @@ by
+ let lemma = fst @@ Lemmas.by
(Proofview.V82.tactic (start_equation f_ref terminate_ref
(fun x ->
prove_eq (fun _ -> tclIDTAC)
@@ -1486,14 +1486,14 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
ih = Id.of_string "______";
}
)
- )) pstate in
- let _ = Flags.silently (fun () -> Lemmas.save_pstate_proved ~pstate ~opaque:opacity ~idopt:None) () in
+ )) lemma in
+ let _ = Flags.silently (fun () -> Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None) () in
()
(* Pp.msgnl (fun _ _ -> str "eqn finished"); *)
let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type_of_f r rec_arg_num eq
- generate_induction_principle using_lemmas : Proof_global.t option =
+ generate_induction_principle using_lemmas : Lemmas.t option =
let open Term in
let open Constr in
let open CVars in
@@ -1550,8 +1550,9 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type
let stop =
(* XXX: What is the correct way to get sign at hook time *)
let sign = Environ.named_context_val Global.(env ()) in
- try com_eqn sign uctx (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);
- false
+ try
+ com_eqn sign uctx (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);
+ false
with e when CErrors.noncritical e ->
begin
if do_observe ()
@@ -1582,15 +1583,15 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type
in
(* XXX STATE Why do we need this... why is the toplevel protection not enough *)
funind_purify (fun () ->
- let pstate = com_terminate
- interactive_proof
- tcc_lemma_name
- tcc_lemma_constr
- is_mes functional_ref
- (EConstr.of_constr rec_arg_type)
- relation rec_arg_num
- term_id
- using_lemmas
- (List.length res_vars)
- evd (Lemmas.mk_hook hook)
- in pstate) ()
+ com_terminate
+ interactive_proof
+ tcc_lemma_name
+ tcc_lemma_constr
+ is_mes functional_ref
+ (EConstr.of_constr rec_arg_type)
+ relation rec_arg_num
+ term_id
+ using_lemmas
+ (List.length res_vars)
+ evd (Lemmas.mk_hook hook))
+ ()
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index b92ac3a0ec..e6aa452def 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -1,23 +1,21 @@
open Constr
-val tclUSER_if_not_mes :
+val tclUSER_if_not_mes :
Tacmach.tactic ->
- bool ->
- Names.Id.t list option ->
+ bool ->
+ Names.Id.t list option ->
Tacmach.tactic
-val recursive_definition :
- interactive_proof:bool ->
- is_mes:bool ->
- Names.Id.t ->
- Constrintern.internalization_env ->
- Constrexpr.constr_expr ->
- Constrexpr.constr_expr ->
- int ->
- Constrexpr.constr_expr ->
- (pconstant ->
- Indfun_common.tcc_lemma_value ref ->
- pconstant ->
- pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) ->
- Constrexpr.constr_expr list ->
- Proof_global.t option
+val recursive_definition
+ : interactive_proof:bool
+ -> is_mes:bool
+ -> Names.Id.t
+ -> Constrintern.internalization_env
+ -> Constrexpr.constr_expr
+ -> Constrexpr.constr_expr
+ -> int
+ -> Constrexpr.constr_expr
+ -> (pconstant -> Indfun_common.tcc_lemma_value ref -> pconstant ->
+ pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit)
+ -> Constrexpr.constr_expr list
+ -> Lemmas.t option
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index b99e77ab2b..2da6584aba 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1962,7 +1962,6 @@ let add_setoid atts binders a aeq t n =
(qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
(qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]
-
let make_tactic name =
let open Tacexpr in
let tacqid = Libnames.qualid_of_string name in
@@ -1988,7 +1987,7 @@ let add_morphism_as_parameter atts m n : unit =
(PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
declare_projection n instance_id (ConstRef cst)
-let add_morphism_interactive atts m n : Proof_global.t =
+let add_morphism_interactive atts m n : Lemmas.t =
warn_add_morphism_deprecated ?loc:m.CAst.loc ();
init_setoid ();
let instance_id = add_suffix n "_Proper" in
@@ -2010,8 +2009,8 @@ let add_morphism_interactive atts m n : Proof_global.t =
let hook = Lemmas.mk_hook hook in
Flags.silently
(fun () ->
- let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
- fst Pfedit.(by (Tacinterp.interp tac) pstate)) ()
+ let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+ fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
let add_morphism atts binders m s n =
init_setoid ();
@@ -2023,12 +2022,12 @@ let add_morphism atts binders m s n =
[cHole; s; m])
in
let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
- let _id, pstate = Classes.new_instance_interactive
+ let _id, lemma = Classes.new_instance_interactive
~global:atts.global atts.polymorphic
instance_name binders instance_t
~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info
in
- pstate (* no instance body -> always open proof *)
+ lemma (* no instance body -> always open proof *)
(** Bind to "rewrite" too *)
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 3ef33c6dc9..a5c3782b30 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -101,16 +101,16 @@ val add_setoid
-> Id.t
-> unit
-val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t
+val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Lemmas.t
val add_morphism_as_parameter : rewrite_attributes -> constr_expr -> Id.t -> unit
val add_morphism
- : rewrite_attributes
+ : rewrite_attributes
-> local_binder_expr list
-> constr_expr
-> constr_expr
-> Id.t
- -> Proof_global.t
+ -> Lemmas.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-01-31 19:12:16 +0000