diff options
| author | msozeau | 2007-03-15 15:51:45 +0000 |
|---|---|---|
| committer | msozeau | 2007-03-15 15:51:45 +0000 |
| commit | 2587079016467becd13b607c24212c16785456a3 (patch) | |
| tree | c2b491c7cca360c8e30e52cad1ef3f1b7d1fedf1 /kernel/type_errors.ml | |
| parent | f4d930d2e7ca21348ac51050c4821fd9c31760ab (diff) | |
Add destruct_call variant where naming of introduced hypotheses is possible. Destruct_exists destructs pairs now.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9705 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions