diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-19 20:21:02 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-19 20:21:02 +0000 |
| commit | f34625ec7bbd0b2b6e2ce02a978d089b47c152ba (patch) | |
| tree | cde02214b20cfa015d3f936d91364a82b2a37990 /test-suite/bugs | |
| parent | ae57ebb1a4d46c8c955940ac1b4c747a6bedcec6 (diff) | |
Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't we
revert the catch of anomalies in reductionops.ml now (commit 13353)?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13439 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2360.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2360.v b/test-suite/bugs/closed/shouldsucceed/2360.v new file mode 100644 index 000000000..b0974a3fd --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2360.v @@ -0,0 +1,13 @@ +(* This failed in V8.3 because descend_in_conjunctions built ill-typed terms *) +Definition interp (etyp : nat -> Type) (p: nat) := etyp p. + +Record Value (etyp : nat -> Type) := Mk { + typ : nat; + value : interp etyp typ +}. + +Definition some_value (etyp : nat -> Type) : (Value etyp). +Proof. + intros. + apply Mk. + |