aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/decl_mode/decl_mode.ml8
-rw-r--r--plugins/decl_mode/decl_mode.mli4
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml43
-rw-r--r--plugins/decl_mode/g_decl_mode.ml414
-rw-r--r--plugins/extraction/extraction.ml4
-rw-r--r--plugins/funind/functional_principles_types.ml8
-rw-r--r--plugins/funind/invfun.ml17
-rw-r--r--plugins/funind/recdef.ml15
-rw-r--r--plugins/setoid_ring/newring.ml418
9 files changed, 66 insertions, 65 deletions
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index 8c5aec38bf..0cbd263168 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -99,11 +99,13 @@ let proof_cond = Proof.no_cond proof_focus
let focus p =
let inf = get_stack p in
- Proof.focus proof_cond inf 1 p
+ Proof_global.with_current_proof (fun _ -> Proof.focus proof_cond inf 1)
-let unfocus = Proof.unfocus proof_focus
+let unfocus () =
+ Proof_global.with_current_proof (fun _ p -> Proof.unfocus proof_focus p ())
-let maximal_unfocus = Proof_global.maximal_unfocus proof_focus
+let maximal_unfocus () =
+ Proof_global.with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus)
let get_top_stack pts =
try
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
index c54dcdc281..8e691f508f 100644
--- a/plugins/decl_mode/decl_mode.mli
+++ b/plugins/decl_mode/decl_mode.mli
@@ -75,6 +75,6 @@ val get_last: Environ.env -> Id.t
val focus : Proof.proof -> unit
-val unfocus : Proof.proof -> unit
+val unfocus : unit -> unit
-val maximal_unfocus : Proof.proof -> unit
+val maximal_unfocus : unit -> unit
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index a06b44083d..e3ef0671c0 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -51,12 +51,13 @@ let _ =
let tcl_change_info_gen info_gen =
(fun gls ->
+ let it, eff = sig_it gls, sig_eff gls in
let concl = pf_concl gls in
- let hyps = Goal.V82.hyps (project gls) (sig_it gls) in
- let extra = Goal.V82.extra (project gls) (sig_it gls) in
+ let hyps = Goal.V82.hyps (project gls) it in
+ let extra = Goal.V82.extra (project gls) it in
let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps concl (info_gen extra) in
- let sigma = Goal.V82.partial_solution sigma (sig_it gls) ev in
- { it = [gl] ; sigma= sigma } )
+ let sigma = Goal.V82.partial_solution sigma it ev in
+ { it = [gl] ; sigma= sigma; eff = eff } )
let tcl_change_info info gls =
let info_gen s = Store.set s Decl_mode.info info in
@@ -128,34 +129,34 @@ let go_to_proof_mode () =
let daimon_tac gls =
set_daimon_flag ();
- {it=[];sigma=sig_sig gls}
+ {it=[];sigma=sig_sig gls;eff=gls.eff}
(* post-instruction focus management *)
(* spiwack: This used to fail if there was no focusing command
above, but I don't think it ever happened. I hope it doesn't mess
things up*)
-let goto_current_focus pts =
- Decl_mode.maximal_unfocus pts
+let goto_current_focus () =
+ Decl_mode.maximal_unfocus ()
-let goto_current_focus_or_top pts =
- goto_current_focus pts
+let goto_current_focus_or_top () =
+ goto_current_focus ()
(* return *)
-let close_tactic_mode pts =
- try goto_current_focus pts
+let close_tactic_mode () =
+ try goto_current_focus ()
with Not_found ->
error "\"return\" cannot be used outside of Declarative Proof Mode."
let return_from_tactic_mode () =
- close_tactic_mode (Proof_global.give_me_the_proof ())
+ close_tactic_mode ()
(* end proof/claim *)
let close_block bt pts =
if Proof.no_focused_goal pts then
- goto_current_focus pts
+ goto_current_focus ()
else
let stack =
if Proof.is_done pts then
@@ -165,7 +166,7 @@ let close_block bt pts =
in
match bt,stack with
B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] ->
- (goto_current_focus pts)
+ (goto_current_focus ())
| _, Claim::_ ->
error "\"end claim\" expected."
| _, Focus_claim::_ ->
@@ -190,13 +191,13 @@ let close_previous_case pts =
match get_top_stack pts with
Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occured ...")
| Suppose_case :: Per (et,_,_,_) :: _ ->
- goto_current_focus (pts)
+ goto_current_focus ()
| _ -> error "Not inside a proof per cases or induction."
else
match get_stack pts with
Per (et,_,_,_) :: _ -> ()
| Suppose_case :: Per (et,_,_,_) :: _ ->
- goto_current_focus ((pts))
+ goto_current_focus ()
| _ -> error "Not inside a proof per cases or induction."
(* Proof instructions *)
@@ -1443,21 +1444,21 @@ let rec postprocess pts instr =
in
try
Inductiveops.control_only_guard env pfterm;
- goto_current_focus_or_top pts
+ goto_current_focus_or_top ()
with
Type_errors.TypeError(env,
Type_errors.IllFormedRecBody(_,_,_,_,_)) ->
anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint")
end
| Pend _ ->
- goto_current_focus_or_top (pts)
+ goto_current_focus_or_top ()
let do_instr raw_instr pts =
let has_tactic = preprocess pts raw_instr.instr in
begin
if has_tactic then
- let { it=gls ; sigma=sigma } = Proof.V82.subgoals pts in
- let gl = { it=List.hd gls ; sigma=sigma } in
+ let { it=gls ; sigma=sigma; eff=eff } = Proof.V82.subgoals pts in
+ let gl = { it=List.hd gls ; sigma=sigma; eff=eff } in
let env= pf_env gl in
let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
gsigma = sigma; genv = env} in
@@ -1469,7 +1470,7 @@ let do_instr raw_instr pts =
postprocess pts raw_instr.instr;
(* spiwack: this should restore a compatible semantics with
v8.3 where we never stayed focused on 0 goal. *)
- Decl_mode.maximal_unfocus pts
+ Decl_mode.maximal_unfocus ()
let proof_instr raw_instr =
let p = Proof_global.give_me_the_proof () in
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 8f570af7e2..072737dab2 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -65,7 +65,7 @@ let vernac_decl_proof () =
if Proof.is_done pf then
Errors.error "Nothing left to prove here."
else
- Proof.transaction pf begin fun () ->
+ begin
Decl_proof_instr.go_to_proof_mode () ;
Proof_global.set_proof_mode "Declarative" ;
Vernacentries.print_subgoals ()
@@ -73,14 +73,14 @@ let vernac_decl_proof () =
(* spiwack: some bureaucracy is not performed here *)
let vernac_return () =
- Proof.transaction (Proof_global.give_me_the_proof ()) begin fun () ->
+ begin
Decl_proof_instr.return_from_tactic_mode () ;
Proof_global.set_proof_mode "Declarative" ;
Vernacentries.print_subgoals ()
end
let vernac_proof_instr instr =
- Proof.transaction (Proof_global.give_me_the_proof ()) begin fun () ->
+ begin
Decl_proof_instr.proof_instr instr;
Vernacentries.print_subgoals ()
end
@@ -397,4 +397,10 @@ GLOBAL: proof_instr;
;
END;;
-
+open Vernacexpr
+
+let () =
+ Vernac_classifier.declare_vernac_classifier "decl_mode" (function
+ | VernacExtend (("DeclProof"|"DeclReturn"), _) -> VtProofStep, VtNow
+ | VernacExtend ("ProofInstr", _) -> VtProofStep, VtLater
+ | _ -> VtUnknown, VtNow)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 5c67c33b6a..68f832997c 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -993,7 +993,7 @@ let extract_constant env kn cb =
| OpaqueDef c ->
add_opaque r;
if access_opaque () then
- mk_typ (Lazyconstr.force_opaque c)
+ mk_typ (Lazyconstr.force_opaque (Future.force c))
else mk_typ_ax ())
| (Info,Default) ->
(match cb.const_body with
@@ -1002,7 +1002,7 @@ let extract_constant env kn cb =
| OpaqueDef c ->
add_opaque r;
if access_opaque () then
- mk_def (Lazyconstr.force_opaque c)
+ mk_def (Lazyconstr.force_opaque (Future.force c))
else mk_ax ())
let extract_constant_spec env kn cb =
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index f70ce00924..efed9a8560 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -339,7 +339,8 @@ let generate_functional_principle
let value = change_property_sort s new_principle_type new_princ_name in
(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
let ce =
- { const_entry_body = value;
+ { const_entry_body =
+ Future.from_val (value,Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = None;
const_entry_opaque = false;
@@ -556,7 +557,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
in
let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in
- let ctxt,fix = decompose_lam_assum first_princ_body in (* the principle has for forall ...., fix .*)
+ let ctxt,fix = decompose_lam_assum (fst(Future.force first_princ_body)) in (* the principle has for forall ...., fix .*)
let (idxs,_),(_,ta,_ as decl) = destFix fix in
let other_result =
List.map (* we can now compute the other principles *)
@@ -598,7 +599,8 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt
in
{const with
- Entries.const_entry_body = princ_body;
+ Entries.const_entry_body =
+ (Future.from_val (princ_body,Declareops.no_seff));
Entries.const_entry_type = Some scheme_type
}
)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index fd074386ec..7d14d1408c 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1013,10 +1013,9 @@ let do_save () = Lemmas.save_named false
*)
let derive_correctness make_scheme functional_induction (funs: constant list) (graphs:inductive list) =
- let previous_state = States.freeze ~marshallable:false in
let funs = Array.of_list funs and graphs = Array.of_list graphs in
let funs_constr = Array.map mkConst funs in
- try
+ States.with_state_protection (fun () ->
let graphs_constr = Array.map mkInd graphs in
let lemmas_types_infos =
Util.Array.map2_i
@@ -1044,7 +1043,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
Array.of_list
(List.map
(fun entry ->
- (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type )
+ (fst(Future.force entry.Entries.const_entry_body), Option.get entry.Entries.const_entry_type )
)
(make_scheme (Array.map_to_list (fun const -> const,GType None) funs))
)
@@ -1122,16 +1121,8 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
let lem_cst = destConst (Constrintern.global_reference lem_id) in
update_Function {finfo with completeness_lemma = Some lem_cst}
)
- funs;
- with reraise ->
- (* In case of problem, we reset all the lemmas *)
- Pfedit.delete_all_proofs ();
- States.unfreeze previous_state;
- raise reraise
-
-
-
-
+ funs)
+ ()
(***********************************************)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 4b9704c2c9..68b291ff96 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -57,7 +57,8 @@ let find_reference sl s =
let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) =
fun f_id kind value ->
- let ce = {const_entry_body = value;
+ let ce = {const_entry_body = Future.from_val
+ (value, Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = None;
const_entry_opaque = false;
@@ -1261,7 +1262,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
ref_ := Some lemma ;
let lid = ref [] in
let h_num = ref (-1) in
- ignore (Flags.silently Vernacentries.interp (Vernacexpr.VernacAbort None));
+ ignore (Flags.silently Vernacentries.interp (Loc.ghost,Vernacexpr.VernacAbort None));
build_proof
( fun gls ->
let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
@@ -1443,7 +1444,6 @@ let (com_eqn : int -> Id.t ->
let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
generate_induction_principle using_lemmas : unit =
- let previous_label = Lib.current_command_label () in
let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
let env = push_named (function_name,None,function_type) (Global.env()) in
(* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
@@ -1513,7 +1513,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
spc () ++ str"is defined" )
)
in
- try
+ States.with_state_protection (fun () ->
com_terminate
tcc_lemma_name
tcc_lemma_constr
@@ -1523,9 +1523,6 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
term_id
using_lemmas
(List.length res_vars)
- hook
- with reraise ->
- ignore (Backtrack.backto previous_label);
- (* anomaly (Pp.str "Cannot create termination Lemma") *)
- raise reraise
+ hook)
+ ()
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index aecbbfe856..be661587ad 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -176,7 +176,7 @@ let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c)
let dummy_goal env =
let (gl,_,sigma) =
Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Evd.Store.empty in
- {Evd.it = gl;
+ {Evd.it = gl; Evd.eff=Declareops.no_seff;
Evd.sigma = sigma}
let exec_tactic env n f args =
@@ -679,8 +679,10 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign div =
let lemma1 = constr_of params.(3) in
let lemma2 = constr_of params.(4) in
- let lemma1 = decl_constant (Id.to_string name^"_ring_lemma1") lemma1 in
- let lemma2 = decl_constant (Id.to_string name^"_ring_lemma2") lemma2 in
+ let lemma1 =
+ decl_constant (Id.to_string name^"_ring_lemma1") (Future.from_val ( lemma1,Declareops.no_seff)) in
+ let lemma2 =
+ decl_constant (Id.to_string name^"_ring_lemma2") (Future.from_val ( lemma2,Declareops.no_seff)) in
let cst_tac =
interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
let pretac =
@@ -1030,11 +1032,11 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odi
match inj with
| Some thm -> mkApp(constr_of params.(8),[|thm|])
| None -> constr_of params.(7) in
- let lemma1 = decl_constant (Id.to_string name^"_field_lemma1") lemma1 in
- let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") lemma2 in
- let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") lemma3 in
- let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") lemma4 in
- let cond_lemma = decl_constant (Id.to_string name^"_lemma5") cond_lemma in
+ let lemma1 = decl_constant (Id.to_string name^"_field_lemma1") (Future.from_val (lemma1,Declareops.no_seff)) in
+ let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") (Future.from_val (lemma2,Declareops.no_seff)) in
+ let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") (Future.from_val (lemma3,Declareops.no_seff)) in
+ let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") (Future.from_val (lemma4,Declareops.no_seff)) in
+ let cond_lemma = decl_constant (Id.to_string name^"_lemma5") (Future.from_val (cond_lemma,Declareops.no_seff)) in
let cst_tac =
interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
let pretac =
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 03:39:44 +0000