diff options
| author | herbelin | 2013-03-21 18:56:11 +0000 |
|---|---|---|
| committer | herbelin | 2013-03-21 18:56:11 +0000 |
| commit | 37a159edcbc1e2088c23592639ba6b12576bce61 (patch) | |
| tree | 6b72915aef65a1d56a78a03041264d77d59e98f2 /kernel/nativecode.mli | |
| parent | e3d808c4aa7387a12aee0d30a64ea85550b82eb8 (diff) | |
Add type information in error message when a constructor is not fully
applied in pattern-matching. This provides with a side way for the
user to understand what is happening in the situation
match ... with ... S ... => ... end" where S is supposed to be a
variable but S being taken by Coq as successor in nat.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16335 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions