diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/decl_mode.ml | 14 | ||||
| -rw-r--r-- | proofs/decl_mode.mli | 13 |
2 files changed, 17 insertions, 10 deletions
diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml index cb148f4e54..b83f9dc658 100644 --- a/proofs/decl_mode.ml +++ b/proofs/decl_mode.ml @@ -41,16 +41,19 @@ let check_not_proof_mode str = error str 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; per_ctype:types; @@ -58,7 +61,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 * identifier list diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli index 412624b4db..6be3abdfe3 100644 --- a/proofs/decl_mode.mli +++ b/proofs/decl_mode.mli @@ -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 |