diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /plugins/decl_mode/decl_mode.mli | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'plugins/decl_mode/decl_mode.mli')
-rw-r--r-- | plugins/decl_mode/decl_mode.mli | 79 |
1 files changed, 0 insertions, 79 deletions
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli deleted file mode 100644 index dfeee833..00000000 --- a/plugins/decl_mode/decl_mode.mli +++ /dev/null @@ -1,79 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Names -open Term -open Evd - -val set_daimon_flag : unit -> unit -val clear_daimon_flag : unit -> unit -val get_daimon_flag : unit -> bool - -type command_mode = - Mode_tactic - | Mode_proof - | Mode_none - -val mode_of_pftreestate : Proof.proof -> command_mode - -val get_current_mode : unit -> command_mode - -val check_not_proof_mode : string -> unit - -type split_tree= - Skip_patt of Id.Set.t * split_tree - | Split_patt of Id.Set.t * inductive * - (bool array * (Id.Set.t * split_tree) option) array - | Close_patt of split_tree - | End_patt of (Id.t * (int * int)) - -type elim_kind = - EK_dep of split_tree - | EK_nodep - | EK_unknown - -type recpath = int option*Declarations.wf_paths - -type per_info = - {per_casee:constr; - per_ctype:types; - per_ind:inductive; - per_pred:constr; - per_args:constr list; - per_params:constr list; - per_nparams:int; - per_wf:recpath} - -type stack_info = - Per of Decl_expr.elim_type * per_info * elim_kind * Names.Id.t list - | Suppose_case - | Claim - | Focus_claim - -type pm_info = - {pm_stack : stack_info list } - -val info : pm_info Store.field - -val get_info : Evd.evar_map -> Proof_type.goal -> pm_info - -val try_get_info : Evd.evar_map -> Proof_type.goal -> pm_info option - -val get_stack : Proof.proof -> stack_info list - -val get_top_stack : Proof.proof -> stack_info list - -val get_last: Environ.env -> Id.t -(** [get_last] raises a [UserError] when it cannot find a previous - statement in the environment. *) - -val get_end_command : Proof.proof -> string - -val focus : Proof.proof -> unit - -val unfocus : unit -> unit |