diff options
| author | herbelin | 2001-06-25 16:43:26 +0000 |
|---|---|---|
| committer | herbelin | 2001-06-25 16:43:26 +0000 |
| commit | 9aa21e481797956087f29ae15603eb1e406b3032 (patch) | |
| tree | 90559c26328e5965819d0fb7f640476717bae6f7 /syntax | |
| parent | e3cf090ffd51d6226a6e0b50e7b264040cab0d7d (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@1808 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'syntax')
| -rw-r--r-- | syntax/PPTactic.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v index 6c0e1a2792..1406b9d233 100644 --- a/syntax/PPTactic.v +++ b/syntax/PPTactic.v @@ -227,7 +227,7 @@ Syntax tactic | decomposeand [<<(DecomposeAnd $c)>>] -> [ "Decompose Record " $c ] | decomposeor [<<(DecomposeOr $c)>>] -> [ "Decompose Sum " $c ] - | decomposethese [<<(DecomposeThese (CLAUSE ($LIST $l)) $c )>>] -> + | decomposethese [<<(DecomposeThese $c ($LIST $l))>>] -> ["Decompose" [1 1] [<hov 0> "[" (LISTSPC ($LIST $l)) "]" ] [1 1] $c] | mutualcofixtactic [<<(Cofix $id $cfe ($LIST $fd))>>] @@ -389,6 +389,10 @@ Syntax tactic | clause_none [<<(CLAUSE)>>] -> [ ] + (* Hypotheses *) + | inhyp [<<(INHYP $x)>>] -> [ $x ] + | inhyptype [<<(INHYPTYPE $x)>>] -> [ "(Type of " $x ")" ] + (* Lists with separators *) | listspc_cons [<<(LISTSPC $x ($LIST $l))>>] -> [ $x [1 0] (LISTSPC ($LIST $l)) ] |