diff options
| author | corbinea | 2007-07-24 13:55:50 +0000 |
|---|---|---|
| committer | corbinea | 2007-07-24 13:55:50 +0000 |
| commit | 0db0531fde66678f60d54df60be1337a7f489000 (patch) | |
| tree | 009323904a2355e610f4735862eeec4d0bf28423 /proofs | |
| parent | 3fbfcfd052fd7e007d50c8ee19e44525f80577ac (diff) | |
Declarative language: fixed the generation of fixpoints for induction proofs.
Cleaner code: the guardedness bug is now corrected.
Added "trivial" to the automation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10042 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |