diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-06-25 13:37:10 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-06-25 13:37:10 +0000 |
| commit | 8ed67d4a2dabe40186c8ad0550fb3fbd2d9b8787 (patch) | |
| tree | 08a302bdd28b98df9da11751b831229ffc21cc04 /tactics/elim.mli | |
| parent | 77259e0b563a10d57b55ac38400ca1843fb938f3 (diff) | |
Les réduction dans les hypothèses s'appliquent maintenant au corps de la définition en cas de LetIn (l'horrible syntaxe 'Unfold toto in (Type of hyp)' permet de forcer la réduction dans le type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/elim.mli')
| -rw-r--r-- | tactics/elim.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/elim.mli b/tactics/elim.mli index e2b9a75e3..c21d4452b 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -29,7 +29,7 @@ val general_decompose : (clause * constr -> bool) -> constr -> tactic val decompose_nonrec : constr -> tactic val decompose_and : constr -> tactic val decompose_or : constr -> tactic -val h_decompose : identifier list -> constr -> tactic +val h_decompose : section_path list -> constr -> tactic val double_ind : int -> int -> tactic |