From 9aa21e481797956087f29ae15603eb1e406b3032 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 25 Jun 2001 16:43:26 +0000 Subject: 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 --- syntax/PPTactic.v | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'syntax') 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] [ "[" (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)) ] -- cgit v1.2.3