aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/tacexpr.mli2
-rw-r--r--kernel/safe_typing.ml2
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/functional_principles_types.ml11
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--plugins/funind/indfun_common.ml2
-rw-r--r--plugins/funind/invfun.ml4
-rw-r--r--plugins/funind/recdef.ml6
-rw-r--r--proofs/pfedit.ml3
-rw-r--r--proofs/pfedit.mli2
-rw-r--r--proofs/proof.ml93
-rw-r--r--proofs/proof_global.ml23
-rw-r--r--proofs/proof_global.mli8
-rw-r--r--tactics/rewrite.ml44
-rw-r--r--tactics/tacinterp.ml1
-rw-r--r--tactics/tactic_option.ml8
-rw-r--r--toplevel/class.ml8
-rw-r--r--toplevel/classes.ml4
-rw-r--r--toplevel/command.ml14
-rw-r--r--toplevel/command.mli3
-rw-r--r--toplevel/lemmas.ml8
-rw-r--r--toplevel/obligations.ml14
-rw-r--r--toplevel/obligations.mli2
-rw-r--r--toplevel/vernacentries.ml6
24 files changed, 109 insertions, 123 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index df4ed2c41..435064b99 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -283,4 +283,4 @@ type raw_tactic_arg =
type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen
-type 'a declaration_hook = locality -> global_reference -> 'a
+type 'a declaration_hook = (locality -> global_reference -> 'a) option
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index eb5c01692..d95e9fe73 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -139,6 +139,8 @@ let join_safe_environment e =
{e with future_cst = []} e.future_cst
(* TODO : out of place and maybe incomplete w.r.t. modules *)
+(* this is there to explore the opaque pre-env structure but is
+ * not part of the trusted code base *)
let prune_env env =
let env = Environ.pre_env env in
let prune_ckey (cb,k) = Declareops.prune_constant_body cb, k in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 6913b40ea..15e284398 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -982,7 +982,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
(mk_equation_id f_id)
(Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
lemma_type
- (fun _ _ -> ());
+ None;
Pfedit.by (prove_replacement);
Lemmas.save_named false
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index efed9a856..a01039eb0 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -329,7 +329,7 @@ let generate_functional_principle
id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
in
let names = ref [new_princ_name] in
- let hook new_principle_type _ _ =
+ let hook new_principle_type = Some (fun _ _ ->
if sorts = None
then
(* let id_of_f = Label.to_id (con_label f) in *)
@@ -357,10 +357,11 @@ let generate_functional_principle
names := name :: !names
in
register_with_sort InProp;
- register_with_sort InSet
+ register_with_sort InSet)
in
let (id,(entry,g_kind,hook)) =
- build_functional_principle interactive_proof old_princ_type new_sorts funs i proof_tac hook
+ build_functional_principle interactive_proof 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 !!!!
@@ -517,7 +518,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
this_block_funs
0
(prove_princ_for_struct false 0 (Array.of_list funs))
- (fun _ _ _ -> ())
+ (fun _ -> None)
with e when Errors.noncritical e ->
begin
begin
@@ -591,7 +592,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
this_block_funs
!i
(prove_princ_for_struct false !i (Array.of_list funs))
- (fun _ _ _ -> ())
+ (fun _ -> None)
in
const
with Found_type i ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 91badbfd7..d1fa16c0a 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -352,7 +352,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
| [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in
Command.do_definition fname (Decl_kinds.Global,Decl_kinds.Definition)
- bl None body (Some ret_type) (fun _ _ -> ())
+ bl None body (Some ret_type) None
| _ ->
Command.do_fixpoint Global fixpoint_exprl
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 4d26c4f53..827747c6b 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -161,7 +161,7 @@ let save with_clean id const (locality,kind) hook =
(locality, ConstRef kn)
in
if with_clean then Pfedit.delete_current_proof ();
- hook l r;
+ Option.default (fun _ _ -> ()) hook l r;
definition_message id
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 7d14d1408..7c70815a6 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1061,7 +1061,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
Lemmas.start_proof lem_id
(Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
(fst lemmas_types_infos.(i))
- (fun _ _ -> ());
+ None;
Pfedit.by
(observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
(proving_tac i));
@@ -1112,7 +1112,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
Lemmas.start_proof lem_id
(Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
(fst lemmas_types_infos.(i))
- (fun _ _ -> ());
+ None;
Pfedit.by
(observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
(proving_tac i));
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 68b291ff9..e6f682635 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1313,7 +1313,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
(Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma)
sign
gls_type
- hook ;
+ (Some hook) ;
if Indfun_common.is_strict_tcc ()
then
by (tclIDTAC)
@@ -1406,7 +1406,7 @@ let (com_eqn : int -> Id.t ->
let f_constr = constr_of_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
(start_proof eq_name (Global, Proof Lemma)
- (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
+ (Environ.named_context_val env) equation_lemma_type None;
by
(start_equation f_ref terminate_ref
(fun x ->
@@ -1523,6 +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)
+ (Some hook))
()
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index ed1de75bc..d02711eeb 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -48,7 +48,6 @@ let get_pftreestate () =
Proof_global.give_me_the_proof ()
let set_end_tac tac =
- let tac = Proofview.V82.tactic tac in
Proof_global.set_endline_tactic tac
let set_used_variables l =
@@ -117,7 +116,7 @@ open Decl_kinds
let next = let n = ref 0 in fun () -> incr n; !n
let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac =
- start_proof id goal_kind sign typ (fun _ _ -> ());
+ start_proof id goal_kind sign typ None;
try
by tac;
let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index ed9b55ae5..79929fd8d 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -122,7 +122,7 @@ val get_all_proof_names : unit -> Id.t list
(** [set_end_tac tac] applies tactic [tac] to all subgoal generate
by [solve_nth] *)
-val set_end_tac : tactic -> unit
+val set_end_tac : Tacexpr.raw_tactic_expr -> unit
(** {6 ... } *)
(** [set_used_variables l] declares that section variables [l] will be
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 38886e9e1..c1a909aed 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -34,13 +34,15 @@ open Util
type _focus_kind = int
type 'a focus_kind = _focus_kind
type focus_info = Obj.t
+type reason = NotThisWay | AlreadyNoFocus
type unfocusable =
- | Cannot of exn
+ | Cannot of reason
| Loose
| Strict
type _focus_condition =
- (_focus_kind -> Proofview.proofview -> unfocusable) *
- (_focus_kind -> bool)
+ | CondNo of bool * _focus_kind
+ | CondDone of bool * _focus_kind
+ | CondEndStack of _focus_kind (* loose_end is false here *)
type 'a focus_condition = _focus_condition
let next_kind = ref 0
@@ -49,51 +51,11 @@ let new_focus_kind () =
incr next_kind;
r
-(* Auxiliary function to define conditions. *)
-let check kind1 kind2 = Int.equal kind1 kind2
-
(* To be authorized to unfocus one must meet the condition prescribed by
the action which focused.*)
(* spiwack: we could consider having a list of authorized focus_kind instead
of just one, if anyone needs it *)
-(* [no_cond] only checks that the unfocusing command uses the right
- [focus_kind]. *)
-
-module Cond = struct
- (* first attempt at an algebra of condition *)
- (* semantics:
- - [Cannot] means that the condition is not met
- - [Strict] that the condition is met
- - [Loose] that the condition is not quite met
- but authorises to unfocus provided a condition
- of a previous focus on the stack is (strictly)
- met. [Loose] focuses are those, like bullets,
- which do not have a closing command and
- are hence closed by unfocusing actions unrelated
- to their focus_kind.
- *)
- let bool e b =
- if b then fun _ _ -> Strict
- else fun _ _ -> Cannot e
- let loose c k p = match c k p with
- | Cannot _ -> Loose
- | c -> c
- let cloose l c =
- if l then loose c
- else c
- let (&&&) c1 c2 k p=
- match c1 k p , c2 k p with
- | Cannot e , _
- | _ , Cannot e -> Cannot e
- | Strict, Strict -> Strict
- | _ , _ -> Loose
- let kind e k0 k p = bool e (Int.equal k0 k) k p
- let pdone e k p = bool e (Proofview.finished p) k p
-end
-
-(* Unfocus command.
- Fails if the proof is not focused. *)
exception CannotUnfocusThisWay
let _ = Errors.register_handler begin function
| CannotUnfocusThisWay ->
@@ -101,18 +63,24 @@ let _ = Errors.register_handler begin function
| _ -> raise Errors.Unhandled
end
-open Cond
-let no_cond_gen e ~loose_end k0 =
- cloose loose_end (kind e k0)
-let no_cond_gen e ?(loose_end=false) k = no_cond_gen e ~loose_end k , check k
-let no_cond ?loose_end = no_cond_gen CannotUnfocusThisWay ?loose_end
-(* [done_cond] checks that the unfocusing command uses the right [focus_kind]
- and that the focused proofview is complete. *)
-let done_cond_gen e ~loose_end k0 =
- (cloose loose_end (kind e k0)) &&& pdone e
-let done_cond_gen e ?(loose_end=false) k = done_cond_gen e ~loose_end k , check k
-let done_cond ?loose_end = done_cond_gen CannotUnfocusThisWay ?loose_end
-
+let check_cond_kind c k =
+ let kind_of_cond = function
+ | CondNo (_,k) | CondDone(_,k) | CondEndStack k -> k in
+ kind_of_cond c = k
+
+let test_cond c k1 pw =
+ match c with
+ | CondNo(_, k) when k = k1 -> Strict
+ | CondNo(true, _) -> Loose
+ | CondNo(false, _) -> Cannot NotThisWay
+ | CondDone(_, k) when k = k1 && Proofview.finished pw -> Strict
+ | CondDone(true, _) -> Loose
+ | CondDone(false, _) -> Cannot NotThisWay
+ | CondEndStack k when k = k1 -> Strict
+ | CondEndStack _ -> Cannot AlreadyNoFocus
+
+let no_cond ?(loose_end=false) k = CondNo (loose_end, k)
+let done_cond ?(loose_end=false) k = CondDone (loose_end,k)
(* Subpart of the type of proofs. It contains the parts of the proof which
are under control of the undo mechanism *)
@@ -207,8 +175,9 @@ let focus cond inf i pr =
let rec unfocus kind pr () =
let cond = cond_of_focus pr in
- match fst cond kind pr.proofview with
- | Cannot e -> raise e
+ match test_cond cond kind pr.proofview with
+ | Cannot NotThisWay -> raise CannotUnfocusThisWay
+ | Cannot AlreadyNoFocus -> raise FullyUnfocused
| Strict ->
let pr = _unfocus pr in
pr
@@ -223,16 +192,16 @@ exception NoSuchFocus
(* no handler: should not be allowed to reach toplevel. *)
let rec get_in_focus_stack kind stack =
match stack with
- | ((_,check),inf,_)::stack ->
- if check kind then inf
+ | (cond,inf,_)::stack ->
+ if check_cond_kind cond kind then inf
else get_in_focus_stack kind stack
| [] -> raise NoSuchFocus
let get_at_focus kind pr =
Obj.magic (get_in_focus_stack kind pr.focus_stack)
let is_last_focus kind pr =
- let ((_,check),_,_) = List.hd pr.focus_stack in
- check kind
+ let (cond,_,_) = List.hd pr.focus_stack in
+ check_cond_kind cond kind
let no_focused_goal p =
Proofview.finished p.proofview
@@ -247,7 +216,7 @@ let rec maximal_unfocus k p =
(* [end_of_stack] is unfocused by return to close every loose focus. *)
let end_of_stack_kind = new_focus_kind ()
-let end_of_stack = done_cond_gen FullyUnfocused end_of_stack_kind
+let end_of_stack = CondEndStack end_of_stack_kind
let unfocused = is_last_focus end_of_stack_kind
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 470d19b71..1f5ee7f75 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -65,13 +65,13 @@ type lemma_possible_guards = int list list
type pstate = {
pid : Id.t;
- endline_tactic : unit Proofview.tactic;
+ endline_tactic : Tacexpr.raw_tactic_expr option;
section_vars : Context.section_context option;
proof : Proof.proof;
strength : Decl_kinds.goal_kind;
compute_guard : lemma_possible_guards;
hook : unit Tacexpr.declaration_hook;
- mode : proof_mode;
+ mode : proof_mode option;
}
(* The head of [!pstates] is the actual current proof, the other ones are
@@ -84,7 +84,7 @@ let current_proof_mode = ref !default_proof_mode
(* combinators for proof modes *)
let update_proof_mode () =
match !pstates with
- | { mode = m } :: _ ->
+ | { mode = Some m } :: _ ->
!current_proof_mode.reset ();
current_proof_mode := m;
!current_proof_mode.set ()
@@ -141,18 +141,25 @@ let cur_pstate () =
let give_me_the_proof () = (cur_pstate ()).proof
let get_current_proof_name () = (cur_pstate ()).pid
+let interp_tac = ref (fun _ _ -> assert false)
+let set_interp_tac f = interp_tac := f
+
let with_current_proof f =
match !pstates with
| [] -> raise NoCurrentProof
| p :: rest ->
- let p = { p with proof = f p.endline_tactic p.proof } in
+ let et =
+ match p.endline_tactic with
+ | None -> Proofview.tclUNIT ()
+ | Some tac -> Proofview.V82.tactic (!interp_tac tac) in
+ let p = { p with proof = f et p.proof } in
pstates := p :: rest
(* Sets the tactic to be used when a tactic line is closed with [...] *)
let set_endline_tactic tac =
match !pstates with
| [] -> raise NoCurrentProof
- | p :: rest -> pstates := { p with endline_tactic = tac } :: rest
+ | p :: rest -> pstates := { p with endline_tactic = Some tac } :: rest
(* spiwack: it might be considered to move error messages away.
Or else to remove special exceptions from Proof_global.
@@ -201,7 +208,7 @@ let set_proof_mode m id =
update_proof_mode ()
let set_proof_mode mn =
- set_proof_mode (find_proof_mode mn) (get_current_proof_name ())
+ set_proof_mode (Some (find_proof_mode mn)) (get_current_proof_name ())
let activate_proof_mode mode = (find_proof_mode mode).set ()
let disactivate_proof_mode mode = (find_proof_mode mode).reset ()
@@ -225,12 +232,12 @@ let start_proof id str goals ?(compute_guard=[]) hook =
let initial_state = {
pid = id;
proof = Proof.start goals;
- endline_tactic = Proofview.tclUNIT ();
+ endline_tactic = None;
section_vars = None;
strength = str;
compute_guard = compute_guard;
hook = hook;
- mode = ! default_proof_mode } in
+ mode = None } in
push initial_state pstates
let get_used_variables () = (cur_pstate ()).section_vars
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 61bb5c0dd..4462255dd 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -82,7 +82,10 @@ val with_current_proof :
(unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit
(** Sets the tactic to be used when a tactic line is closed with [...] *)
-val set_endline_tactic : unit Proofview.tactic -> unit
+val set_endline_tactic : Tacexpr.raw_tactic_expr -> unit
+val set_interp_tac :
+ (Tacexpr.raw_tactic_expr -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma)
+ -> unit
(** Sets the section variables assumed by the proof *)
val set_used_variables : Names.Id.t list -> unit
@@ -136,7 +139,8 @@ module Bullet : sig
end
module V82 : sig
- val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list * Decl_kinds.goal_kind * unit Tacexpr.declaration_hook)
+ val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list *
+ Decl_kinds.goal_kind * unit Tacexpr.declaration_hook)
end
type state
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index c855486db..7a135bef0 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1825,12 +1825,12 @@ let add_morphism_infer glob m n =
Flags.silently
(fun () ->
Lemmas.start_proof instance_id kind instance
- (fun _ -> function
+ (Some (fun _ -> function
Globnames.ConstRef cst ->
add_instance (Typeclasses.new_instance (Lazy.force proper_class) None
glob (ConstRef cst));
declare_projection n instance_id (ConstRef cst)
- | _ -> assert false);
+ | _ -> assert false));
Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) ()
let add_morphism glob binders m s n =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d8e03265d..71312259e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1969,6 +1969,7 @@ let interp_tac_gen lfun avoid_ids debug t gl =
gsigma = project gl; genv = pf_env gl } t) gl
let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
+let _ = Proof_global.set_interp_tac interp
let eval_ltac_constr gl t =
interp_ltac_constr (default_ist ()) gl
diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml
index fdd5a9aae..9acf26f62 100644
--- a/tactics/tactic_option.ml
+++ b/tactics/tactic_option.ml
@@ -14,13 +14,13 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name =
let default_tactic_expr : Tacexpr.glob_tactic_expr ref =
Summary.ref default ~name:(name^"-default-tacexpr")
in
- let default_tactic : Proof_type.tactic ref =
- Summary.ref (Tacinterp.eval_tactic !default_tactic_expr) ~name:(name^"-default-tactic")
+ let default_tactic : Tacexpr.glob_tactic_expr ref =
+ Summary.ref !default_tactic_expr ~name:(name^"-default-tactic")
in
let set_default_tactic local t =
locality := local;
default_tactic_expr := t;
- default_tactic := Tacinterp.eval_tactic t
+ default_tactic := t
in
let cache (_, (local, tac)) = set_default_tactic local tac in
let load (_, (local, tac)) =
@@ -43,7 +43,7 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name =
set_default_tactic local tac;
Lib.add_anonymous_leaf (input (local, tac))
in
- let get () = !locality, !default_tactic in
+ let get () = !locality, Tacinterp.eval_tactic !default_tactic in
let print () =
Pptactic.pr_glob_tactic (Global.env ()) !default_tactic_expr ++
(if !locality then str" (locally defined)" else str" (globally defined)")
diff --git a/toplevel/class.ml b/toplevel/class.ml
index f9ce75bba..89cf116ca 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -297,7 +297,7 @@ let try_add_new_identity_coercion id ~local ~source ~target =
let try_add_new_coercion_with_source ref ~local ~source =
try_add_new_coercion_core ref ~local (Some source) None false
-let add_coercion_hook local ref =
+let add_coercion_hook = Some (fun local ref ->
let stre = match local with
| Local -> true
| Global -> false
@@ -305,13 +305,13 @@ let add_coercion_hook local ref =
in
let () = try_add_new_coercion ref stre in
let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
- Flags.if_verbose msg_info msg
+ Flags.if_verbose msg_info msg)
-let add_subclass_hook local ref =
+let add_subclass_hook = Some (fun local ref ->
let stre = match local with
| Local -> true
| Global -> false
| Discharge -> assert false
in
let cl = class_of_global ref in
- try_add_new_coercion_subclass cl stre
+ try_add_new_coercion_subclass cl stre)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index a217abbba..fa5d405e2 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -292,13 +292,13 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
| None -> [||], None, termtype
in
ignore (Obligations.add_definition id ?term:constr
- typ ~kind:(Global,Instance) ~hook obls);
+ typ ~kind:(Global,Instance) ~hook:(Some hook) obls);
id
else
(Flags.silently
(fun () ->
Lemmas.start_proof id kind termtype
- (fun _ -> instance_hook k pri global imps ?hook);
+ (Some (fun _ -> instance_hook k pri global imps ?hook));
if not (Option.is_empty term) then
Pfedit.by (!refine_ref (evm, Option.get term))
else if Flags.is_auto_intros () then
diff --git a/toplevel/command.ml b/toplevel/command.ml
index d730d8ef1..9f24fc158 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -152,7 +152,7 @@ let declare_definition ident (local,k) ce imps hook =
VarRef ident
| Discharge | Local | Global ->
declare_global_definition ident ce local k imps in
- hook local r
+ Option.default (fun _ r -> r) hook local r
let _ = Obligations.declare_definition_ref := declare_definition
@@ -172,7 +172,8 @@ let do_definition ident k bl red_option c ctypopt hook =
in
ignore(Obligations.add_definition ident ~term:c cty ~implicits:imps ~kind:k ~hook obls)
else let ce = check_definition def in
- declare_definition ident k ce imps hook
+ ignore(declare_definition ident k ce imps
+ (Option.map (fun f l r -> f l r;r) hook))
(* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
@@ -530,7 +531,7 @@ let declare_fix kind f def t imps =
const_entry_opaque = false;
const_entry_inline_code = false
} in
- declare_definition f kind ce imps (fun _ r -> r)
+ declare_definition f kind ce imps None
let _ = Obligations.declare_fix_ref := declare_fix
@@ -742,7 +743,8 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
let evars, _, evars_def, evars_typ =
Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp
in
- ignore(Obligations.add_definition recname ~term:evars_def evars_typ evars ~hook)
+ ignore(Obligations.add_definition
+ recname ~term:evars_def evars_typ evars ~hook:(Some hook))
let interp_recursive isfix fixl notations =
@@ -822,7 +824,7 @@ let declare_fixpoint local ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
fixdefs) in
Lemmas.start_proof_with_initialization (Global,DefinitionBody Fixpoint)
- (Some(false,indexes,init_tac)) thms None (fun _ _ -> ())
+ (Some(false,indexes,init_tac)) thms None None
else begin
(* We shortcut the proof process *)
let fixdefs = List.map Option.get fixdefs in
@@ -849,7 +851,7 @@ let declare_cofixpoint local ((fixnames,fixdefs,fixtypes),fiximps) ntns =
Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
fixdefs) in
Lemmas.start_proof_with_initialization (Global,DefinitionBody CoFixpoint)
- (Some(true,[],init_tac)) thms None (fun _ _ -> ())
+ (Some(true,[],init_tac)) thms None None
else begin
(* We shortcut the proof process *)
let fixdefs = List.map Option.get fixdefs in
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 76a3c5802..fe6a0a400 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -35,7 +35,8 @@ val interp_definition :
constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits
val declare_definition : Id.t -> definition_kind ->
- definition_entry -> Impargs.manual_implicits -> 'a declaration_hook -> 'a
+ definition_entry -> Impargs.manual_implicits ->
+ Globnames.global_reference declaration_hook -> Globnames.global_reference
val do_definition : Id.t -> definition_kind ->
local_binder list -> red_expr option -> constr_expr ->
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 6876483a0..846714db7 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -183,7 +183,7 @@ let save ?proof id const do_guard (locality,kind) hook =
(* if the proof is given explicitly, nothing has to be deleted *)
if proof = None then Pfedit.delete_current_proof ();
definition_message id;
- hook l r
+ Option.iter (fun f -> f l r) hook
let default_thm_id = Id.of_string "Unnamed_thm"
@@ -341,8 +341,8 @@ let start_proof_with_initialization kind recguard thms snl hook =
let thms_data = (strength,ref,imps)::other_thms_data in
List.iter (fun (strength,ref,imps) ->
maybe_declare_manual_implicits false ref imps;
- hook strength ref) thms_data in
- start_proof id kind t ?init_tac hook ~compute_guard:guard
+ Option.iter (fun f -> f strength ref) hook) thms_data in
+ start_proof id kind t ?init_tac (Some hook) ~compute_guard:guard
let start_proof_com kind thms hook =
let evdref = ref Evd.empty in
@@ -368,7 +368,7 @@ let admit () =
let kn = declare_constant id (ParameterEntry e,IsAssumption Conjectural) in
Pfedit.delete_current_proof ();
assumption_message id;
- hook Global (ConstRef kn)
+ Option.iter (fun f -> f Global (ConstRef kn)) hook
(* Miscellaneous *)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 9e7ddd5a6..58201a5f8 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -511,7 +511,7 @@ let declare_definition prg =
progmap_remove prg;
!declare_definition_ref prg.prg_name
prg.prg_kind ce prg.prg_implicits
- (fun local gr -> prg.prg_hook local gr; gr)
+ (Option.map (fun f l r -> f l r;r) prg.prg_hook)
open Pp
@@ -579,7 +579,7 @@ let declare_mutual_definition l =
Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
let gr = List.hd kns in
let kn = match gr with ConstRef kn -> kn | _ -> assert false in
- first.prg_hook (fst first.prg_kind) gr;
+ Option.iter (fun f -> f (fst first.prg_kind) gr) first.prg_hook;
List.iter progmap_remove l; kn
let shrink_body c =
@@ -771,7 +771,7 @@ let rec solve_obligation prg num tac =
| [] ->
let obl = subst_deps_obl obls obl in
Lemmas.start_proof obl.obl_name (kind_of_opacity obl.obl_status) obl.obl_type
- (fun strength gr ->
+ (Some (fun strength gr ->
let cst = match gr with ConstRef cst -> cst | _ -> assert false in
let obl =
let transparent = evaluable_constant cst (Global.env ()) in
@@ -801,11 +801,11 @@ let rec solve_obligation prg num tac =
let deps = dependencies obls num in
if not (Int.Set.is_empty deps) then
ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps)
- | _ -> ());
+ | _ -> ()));
trace (str "Started obligation " ++ int user_num ++ str " proof: " ++
Printer.pr_constr_env (Global.env ()) obl.obl_type);
Pfedit.by (snd (get_default_tactic ()));
- Option.iter (fun tac -> Pfedit.set_end_tac (Tacinterp.interp tac)) tac
+ Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
| l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
@@ -923,7 +923,7 @@ let show_term n =
++ Printer.pr_constr_env (Global.env ()) prg.prg_body)
let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
- ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
+ ?(reduce=reduce) ?(hook=None) obls =
let info = str (Id.to_string n) ++ str " has type-checked" in
let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in
let obls,_ = prg.prg_obligations in
@@ -941,7 +941,7 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
| _ -> res)
let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce)
- ?(hook=fun _ _ -> ()) notations fixkind =
+ ?(hook=None) notations fixkind =
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
List.iter
(fun (n, b, t, imps, obls) ->
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index ddc99a96c..081871fce 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -74,7 +74,7 @@ val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types ->
?kind:Decl_kinds.definition_kind ->
?tactic:Proof_type.tactic ->
?reduce:(Term.constr -> Term.constr) ->
- ?hook:(unit Tacexpr.declaration_hook) -> obligation_info -> progress
+ ?hook:unit Tacexpr.declaration_hook -> obligation_info -> progress
type notations =
(Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5316e9d46..bc74c7211 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -414,11 +414,11 @@ let start_proof_and_print k l hook =
start_proof_com k l hook;
print_subgoals ()
-let no_hook _ _ = ()
+let no_hook = None
let vernac_definition_hook = function
| Coercion -> Class.add_coercion_hook
-| CanonicalStructure -> fun _ -> Recordops.declare_canonical_structure
+| CanonicalStructure -> Some (fun _ -> Recordops.declare_canonical_structure)
| SubClass -> Class.add_subclass_hook
| _ -> no_hook
@@ -797,7 +797,7 @@ let vernac_set_end_tac tac =
error "Unknown command of the non proof-editing mode.";
match tac with
| Tacexpr.TacId [] -> ()
- | _ -> set_end_tac (Tacinterp.interp tac)
+ | _ -> set_end_tac tac
(* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
let vernac_set_used_variables l =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 17:51:53 +0000