diff options
| author | lmamane | 2008-02-22 13:39:13 +0000 |
|---|---|---|
| committer | lmamane | 2008-02-22 13:39:13 +0000 |
| commit | e8ef565dadd110329f806fa3c281055fcd807440 (patch) | |
| tree | e0f069cb228ee77524800d98c53291014c1a1315 /toplevel/command.mli | |
| parent | 2e67ff1b33d05b9efc020de664f3200f9ff0d479 (diff) | |
Merge with lmamane's private branch:
- New vernac command "Delete"
- New vernac command "Undo To"
- Added a few hooks used by new contrib/interface
- Beta/incomplete version of dependency generation and dumping
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.mli')
| -rw-r--r-- | toplevel/command.mli | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index 7ec29e0f59..2dbc295387 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -30,6 +30,8 @@ open Redexpr functions of [Declare]; they return an absolute reference to the defined object *) +val set_declare_definition_hook : (Entries.definition_entry -> unit) -> unit + val definition_message : identifier -> unit val declare_definition : identifier -> definition_kind -> @@ -41,6 +43,8 @@ val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> bool -> Names.variable located -> unit +val set_declare_assumption_hook : (types -> unit) -> unit + val declare_assumption : identifier located list -> coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> bool ->unit @@ -93,12 +97,18 @@ val generalize_constr_expr : constr_expr -> local_binder list -> constr_expr val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr -val start_proof : identifier -> goal_kind -> constr -> +(* A hook start_proof calls on the type of the definition being started *) +val set_start_hook : (types -> unit) -> unit + +val start_proof : identifier -> goal_kind -> types -> declaration_hook -> unit val start_proof_com : identifier option -> goal_kind -> (local_binder list * constr_expr) -> declaration_hook -> unit +(* A hook the next three functions pass to cook_proof *) +val set_save_hook : (Refiner.pftreestate -> unit) -> unit + (*s [save_named b] saves the current completed proof under the name it was started; boolean [b] tells if the theorem is declared opaque; it fails if the proof is not completed *) |