diff options
| author | letouzey | 2007-07-06 13:29:54 +0000 |
|---|---|---|
| committer | letouzey | 2007-07-06 13:29:54 +0000 |
| commit | d3eb7c916077eba740d9f35b6ac10358eb0fe934 (patch) | |
| tree | 877cf4de4d51857af42766d8e95ad19e5bb7080b /kernel/type_errors.mli | |
| parent | d5c316353ed1bb63821c511eade468a133a2b480 (diff) | |
Suggestion of additional syntax for intro patterns:
intros {A,B,C,D}
means:
intros (A,(B,(C,D)))
Should be especially useful when breaking existential hypthesis like
{n:nat | P n /\ Q n /\ R n }, hence the notation {}.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9948 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions