diff options
| author | msozeau | 2013-08-23 15:40:57 +0000 |
|---|---|---|
| committer | msozeau | 2013-08-23 15:40:57 +0000 |
| commit | c15c10908f764c7b1016f699160bfaba4e7e848a (patch) | |
| tree | f69c692dabb4e10c5837e00f0456652dbcec30f8 /checker/votour.ml | |
| parent | 9fbe74a0799625fb2f43ec503b2ba8c89bb5aaea (diff) | |
Fix computation of discharged hyps for inductive types forgetting the conclusion of the arity.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16732 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/votour.ml')
0 files changed, 0 insertions, 0 deletions