diff options
Diffstat (limited to 'plugins/decl_mode/decl_mode.mli')
| -rw-r--r-- | plugins/decl_mode/decl_mode.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli index f23a97b4e..853135f10 100644 --- a/plugins/decl_mode/decl_mode.mli +++ b/plugins/decl_mode/decl_mode.mli @@ -27,11 +27,11 @@ val get_current_mode : unit -> command_mode val check_not_proof_mode : string -> unit type split_tree= - Skip_patt of Idset.t * split_tree - | Split_patt of Idset.t * inductive * - (bool array * (Idset.t * split_tree) option) array + 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 (identifier * (int * int)) + | End_patt of (Id.t * (int * int)) type elim_kind = EK_dep of split_tree @@ -51,7 +51,7 @@ type per_info = per_wf:recpath} type stack_info = - Per of Decl_expr.elim_type * per_info * elim_kind * Names.identifier list + Per of Decl_expr.elim_type * per_info * elim_kind * Names.Id.t list | Suppose_case | Claim | Focus_claim @@ -69,7 +69,7 @@ val get_stack : Proof.proof -> stack_info list val get_top_stack : Proof.proof -> stack_info list -val get_last: Environ.env -> identifier +val get_last: Environ.env -> Id.t val focus : Proof.proof -> unit |