diff options
| author | herbelin | 2000-12-20 19:42:17 +0000 |
|---|---|---|
| committer | herbelin | 2000-12-20 19:42:17 +0000 |
| commit | 296fb02406b92203339e6493ede9b9ef0d65075b (patch) | |
| tree | c4315a87774cee569cb11af38bbde811278f348b | |
| parent | dd8b4d6384b0db16e54877ea7d2487deff48e934 (diff) | |
Toujours Induction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1168 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tactics.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5469ad521c..10d6f57e93 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -355,7 +355,7 @@ let rec intros_until s g = ((tclTHEN (reduce (Red true) []) (intros_until s)) g) with Redelimination -> errorlabstrm "Intros" - [<'sTR "No such hypothesis in current goal"; + [<'sTR ("No hypothesis "^(string_of_id s)^" in current goal"); 'sTR " even after head-reduction" >] let rec intros_until_n_gen red n g = @@ -367,7 +367,8 @@ let rec intros_until_n_gen red n g = ((tclTHEN (reduce (Red true) []) (intros_until_n_gen red n)) g) with Redelimination -> errorlabstrm "Intros" - [<'sTR "No such hypothesis in current goal"; + [<'sTR ("No "^(string_of_int n)); + 'sTR "th non dependent hypothesis in current goal"; 'sTR " even after head-reduction" >] else errorlabstrm "Intros" [<'sTR "No such hypothesis in current goal" >] @@ -1349,9 +1350,13 @@ let induction_with_atomization_of_ind_arg hyp0 = let new_induct c gl = match kind_of_term c with | IsVar id when not (mem_named_context id (Global.named_context())) -> +(* tclORELSE (tclTHEN (intros_until id) (tclLAST_HYP simplest_elim)) (induction_with_atomization_of_ind_arg id) gl +*) + tclTHEN (tclTRY (intros_until id)) + (induction_with_atomization_of_ind_arg id) gl | _ -> let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) Anonymous in |