diff options
| author | herbelin | 2001-06-25 13:37:10 +0000 |
|---|---|---|
| committer | herbelin | 2001-06-25 13:37:10 +0000 |
| commit | 8ed67d4a2dabe40186c8ad0550fb3fbd2d9b8787 (patch) | |
| tree | 08a302bdd28b98df9da11751b831229ffc21cc04 /tactics/hiddentac.ml | |
| 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/hiddentac.ml')
| -rw-r--r-- | tactics/hiddentac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 2c4f80b748..bc07c9a4d6 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -13,7 +13,7 @@ open Proof_type open Tacmach open Tacentries -let h_clear ids = v_clear [(Clause ids)] +let h_clear ids = v_clear [(Clause (List.map (fun x -> InHyp x) ids))] let h_move dep id1 id2 = (if dep then v_move else v_move_dep) [Identifier id1;Identifier id2] let h_contradiction = v_contradiction [] |