diff options
Diffstat (limited to 'proofs/decl_mode.mli')
| -rw-r--r-- | proofs/decl_mode.mli | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli index 81fab168..77bee313 100644 --- a/proofs/decl_mode.mli +++ b/proofs/decl_mode.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: decl_mode.mli 10739 2008-04-01 14:45:20Z herbelin $ *) open Names open Term @@ -29,16 +29,18 @@ val get_current_mode : unit -> command_mode val check_not_proof_mode : string -> unit type split_tree= - Push of (Idset.t * split_tree) - | Split of (Idset.t * inductive * (Idset.t*split_tree) option array) - | Pop of split_tree - | End_of_branch of (identifier * int) + Skip_patt of Idset.t * split_tree + | Split_patt of Idset.t * inductive * + (bool array * (Idset.t * split_tree) option) array + | Close_patt of split_tree + | End_patt of (identifier * 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; @@ -47,7 +49,8 @@ type per_info = per_pred:constr; per_args:constr list; per_params:constr list; - per_nparams:int} + per_nparams:int; + per_wf:recpath} type stack_info = Per of Decl_expr.elim_type * per_info * elim_kind * Names.identifier list @@ -56,10 +59,7 @@ type stack_info = | Focus_claim type pm_info = - { pm_last: (Names.identifier * bool) option (* anonymous if none *); - pm_partial_goal : constr ; (* partial goal construction *) - pm_subgoals : (metavariable*constr) list; - pm_stack : stack_info list } + {pm_stack : stack_info list } val pm_in : pm_info -> Dyn.t @@ -70,3 +70,5 @@ val get_end_command : pftreestate -> string option val get_stack : pftreestate -> stack_info list val get_top_stack : pftreestate -> stack_info list + +val get_last: Environ.env -> identifier |